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

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
x : (leftRegular k G).IntertwiningMap σ
x✝ : G
⊢ (((fun v ↦
              { toLinearMap := ((Finsupp.llift V k k G) fun g ↦ (σ g) v) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                isIntertwining' := ⋯ })
            ((fun f ↦ (Finsupp.llift V k k G).symm (f.toLinearMap ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k).symm) 1)
              x)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    (x.toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
;

Goal state after:
k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
x : (leftRegular k G).IntertwiningMap σ
x✝ : G
⊢ (((fun v ↦
              { toLinearMap := ((Finsupp.llift V k k G) fun g ↦ (σ g) v) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                isIntertwining' := ⋯ })
            ((fun f ↦ (Finsupp.llift V k k G).symm (f.toLinearMap ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k).symm) 1)
              x)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    (x.toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ rexp (↑cX * t ^ 2 / 2 + ↑cY * t ^ 2 / 2) = rexp ((↑cX + ↑cY) * t ^ 2 / 2)

Tactic:
;

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ rexp (↑cX * t ^ 2 / 2 + ↑cY * t ^ 2 / 2) = rexp ((↑cX + ↑cY) * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ ↑cX * t ^ 2 / 2 + ↑cY * t ^ 2 / 2 = (↑cX + ↑cY) * t ^ 2 / 2

Tactic:
;

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ ↑cX * t ^ 2 / 2 + ↑cY * t ^ 2 / 2 = (↑cX + ↑cY) * t ^ 2 / 2
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✝⁷ : Semiring 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
hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)
g : G
v : V
⊢ (f ∘ₗ ρ g) v = (σ g ∘ₗ f) v

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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
hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)
g : G
v : V
⊢ (f ∘ₗ ρ g) v = (σ g ∘ₗ f) v
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk
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
g : ρ.IntertwiningMap σ
toLinearMap✝ : V →ₗ[A] W
isIntertwining'✝ : ∀ (g : G), toLinearMap✝ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝
h : { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ }.toLinearMap = g.toLinearMap
⊢ { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ } = g

Tactic:
;

Goal state after:
case mk
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
g : ρ.IntertwiningMap σ
toLinearMap✝ : V →ₗ[A] W
isIntertwining'✝ : ∀ (g : G), toLinearMap✝ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝
h : { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ }.toLinearMap = g.toLinearMap
⊢ { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ } = g
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✝⁷ : Semiring 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 σ
n : ℕ
⊢ ⇑(n • f) = n • ⇑f

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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 σ
n : ℕ
⊢ ⇑(n • f) = n • ⇑f
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✝⁷ : Semiring 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₁ f₂ : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ ((f₁ + f₂).comp g).toLinearMap = (f₁.comp g + f₂.comp g).toLinearMap

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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₁ f₂ : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ ((f₁ + f₂).comp g).toLinearMap = (f₁.comp g + f₂.comp 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✝⁷ : Semiring 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 : σ.IntertwiningMap τ
g₁ g₂ : ρ.IntertwiningMap σ
⊢ (f.comp (g₁ + g₂)).toLinearMap = (f.comp g₁ + f.comp g₂).toLinearMap

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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 : σ.IntertwiningMap τ
g₁ g₂ : ρ.IntertwiningMap σ
⊢ (f.comp (g₁ + g₂)).toLinearMap = (f.comp g₁ + f.comp 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✝⁷ : Semiring 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 : σ.IntertwiningMap τ
g₁ g₂ : ρ.IntertwiningMap σ
⊢ (f.comp (g₁ + g₂)).toLinearMap = (f.comp g₁ + f.comp g₂).toLinearMap

Tactic:
simp [LinearMap.comp_add]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'
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 ρ
toIntertwiningMap✝ : σ.IntertwiningMap ρ
invFun✝ : V → W
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.toLinearEquiv =
    ψ.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ψ

Tactic:
;

Goal state after:
case mk'
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 ρ
toIntertwiningMap✝ : σ.IntertwiningMap ρ
invFun✝ : V → W
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.toLinearEquiv =
    ψ.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ψ
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'.mk'
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
toIntertwiningMap✝¹ : σ.IntertwiningMap ρ
invFun✝¹ : V → W
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : σ.IntertwiningMap ρ
invFun✝ : V → W
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
        right_inv := right_inv✝¹ }.toLinearEquiv =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
;

Goal state after:
case mk'.mk'
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
toIntertwiningMap✝¹ : σ.IntertwiningMap ρ
invFun✝¹ : V → W
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : σ.IntertwiningMap ρ
invFun✝ : V → W
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
        right_inv := right_inv✝¹ }.toLinearEquiv =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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
φ ψ : ρ.Equiv σ
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h1 :
  ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
          right_inv := right_inv✝ }.toLinearEquiv =
    ⇑ψ.toLinearEquiv
h2 :
  { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.invFun =
    ψ.invFun
⊢ { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ψ

Tactic:
;

Goal state after:
case mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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
φ ψ : ρ.Equiv σ
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h1 :
  ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
          right_inv := right_inv✝ }.toLinearEquiv =
    ⇑ψ.toLinearEquiv
h2 :
  { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.invFun =
    ψ.invFun
⊢ { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ψ
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'
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 σ
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h : ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ⇑ψ
⊢ { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ψ

Tactic:
;

Goal state after:
case mk'
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 σ
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h : ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ⇑ψ
⊢ { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = ψ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : 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 ∂μ
⊢ μ.real {ω | X ω ≤ Y ω} ≤ rexp (-(∫ (x : Ω), Y x ∂μ - ∫ (x : Ω), X x ∂μ) ^ 2 / (2 * (↑cX + ↑cY)))

Tactic:
calc μ.real {ω | X ω ≤ Y ω}
  _ = μ.real {ω | (μ[X] - μ[Y]) ≤ (Y ω - μ[Y]) - (X ω - μ[X])} := by
    congr with ω
    grind
  _ ≤ Real.exp (- (μ[Y] - μ[X]) ^ 2 / (2 * (cX + cY))) := by
    refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_
    · rw [add_comm cX]
      refine sub_of_indepFun hY hX ?_
      exact hindep.symm.comp (φ := fun x ↦ x - μ[Y]) (ψ := fun x ↦ x - μ[X])
        (by fun_prop) (by fun_prop)
    · grind
    · congr 2
      grind

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 σ
x✝ : V
⊢ (φ.trans φ.symm) x✝ = (refl ρ) x✝

Tactic:
;

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 σ
x✝ : W
⊢ (φ.symm.trans φ) x✝ = (refl σ) x✝

Tactic:
;

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

Goal state after:
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))
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 σ
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✝

Tactic:
;

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

Tactic:
;

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 : ρ.asModule →ₗ[A[G]] σ.asModule
g : G
v : V
⊢ ({ toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ ρ g) v = (σ g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ }) v

Tactic:
;

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 : ρ.asModule →ₗ[A[G]] σ.asModule
g : G
v : V
⊢ ({ toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ ρ g) v = (σ g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ }) v
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ ∫ (x : Ω), -X x ∂μ = 0

Tactic:
;

Goal state after:
case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ ∫ (x : Ω), -X x ∂μ = 0
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 τ
g : ρ.IntertwiningMap σ
γ : G
v : V
⊢ (f.toLinearMap ∘ₗ g.toLinearMap) ((ρ γ) v) = (τ γ) ((f.toLinearMap ∘ₗ g.toLinearMap) v)

Tactic:
;

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 τ
g : ρ.IntertwiningMap σ
γ : G
v : V
⊢ (f.toLinearMap ∘ₗ g.toLinearMap) ((ρ γ) v) = (τ γ) ((f.toLinearMap ∘ₗ g.toLinearMap) v)