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

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n k : ℕ
p : ↑I
⊢ Bin(R, n, p).real {↑k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

Tactic:
by
  rw [map_measureReal_apply (by fun_prop) (by measurability)]
  convert binomial_real_singleton n k p
  ext; simp

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (n : ℕ) → X n), A.indicator (fun x_1 ↦ f x_1 x) (frestrictLe b x) ∂(traj κ a) u =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f (frestrictLe b y) y ∂(traj κ a) u

Tactic:
simp_rw [← Set.indicator_comp_right, ← integral_indicator (measurable_frestrictLe b hA)]

Goal state after:
X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (n : ℕ) → X n), (frestrictLe b ⁻¹' A).indicator ((fun x_1 ↦ f x_1 x) ∘ frestrictLe b) x ∂(traj κ a) u =
    ∫ (x : (i : ℕ) → X i), (frestrictLe b ⁻¹' A).indicator (fun y ↦ f (frestrictLe b y) y) x ∂(traj κ a) u
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a

Tactic:
· classical exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (⇑μ.toPMF) x = μ s

Tactic:
← μ.tsum_indicator_apply_singleton s hs

Goal state after:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (⇑μ.toPMF) x = ∑' (x : α), s.indicator (fun x ↦ μ {x}) x
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ -(r * x) ≤ 0

Tactic:
by nlinarith

Goal state after:
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
← ht0

Goal state after:
case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case hf
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ 0 ≤ᵐ[volume.restrict (Ici t)] fun x ↦ r * t ^ r * x ^ (-(r + 1))

pp: case hfm
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ AEStronglyMeasurable (fun x ↦ r * t ^ r * x ^ (-(r + 1))) (volume.restrict (Ici t))

Tactic:
· rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]
    filter_upwards with x hx using by positivity [lt_of_lt_of_le ht hx]

Goal state after:
case hfm
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ AEStronglyMeasurable (fun x ↦ r * t ^ r * x ^ (-(r + 1))) (volume.restrict (Ici t))
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (pure a).toMeasure s = (Measure.dirac a) s

Tactic:
rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]

Goal state after:
α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = s.indicator 1 a
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r₁ r₂ : ℝ≥0
⊢ charFun (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) = charFun Po(ℝ, r₁ + r₂)

Tactic:
ext t

Goal state after:
r₁ r₂ : ℝ≥0
t : ℝ
⊢ charFun (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) t = charFun Po(ℝ, r₁ + r₂) t
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r₁ r₂ : ℝ≥0
⊢ Measure.map Nat.cast (Po(r₁) ∗ Po(r₂)) = Po(ℝ, r₁ + r₂)

Tactic:
rw [← Nat.coe_castAddMonoidHom, Measure.map_conv_addMonoidHom _ (by fun_prop)]

Goal state after:
r₁ r₂ : ℝ≥0
⊢ Measure.map ⇑(Nat.castAddMonoidHom ℝ) Po(r₁) ∗ Measure.map ⇑(Nat.castAddMonoidHom ℝ) Po(r₂) =
    Measure.map ⇑(Nat.castAddMonoidHom ℝ) Po(r₁ + r₂)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
⊢ ⨆ i, ⨆ (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n

Tactic:
rw [iSup_exists]

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case mp
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i = s i) →
        μ[(⋂ i ∈ s_1, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ x ∈ s_1, μ[(s x).indicator fun ω ↦ 1 | m']) →
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

pp: case mpr
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']) →
    ∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i = s i) →
        μ[(⋂ i ∈ s_1, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ x ∈ s_1, μ[(s x).indicator fun ω ↦ 1 | m']

Tactic:
· intros
      simp [*]

Goal state after:
case mpr
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']) →
    ∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i = s i) →
        μ[(⋂ i ∈ s_1, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ x ∈ s_1, μ[(s x).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Kernel.swap X.carrier X.carrier ∘ₖ Kernel.copy X.carrier = Kernel.copy X.carrier

Tactic:
exact Kernel.swap_copy

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    Measure.map (fun ω ↦ (ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'

Tactic:
condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun ω ↦ (f ω, g ω)) =
      μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) ↔
    Measure.map (fun ω ↦ (ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ‖X a‖ ^ ↑p ∂μ.tilted fun x ↦ t * X x) < ∞

Tactic:
norm_eq_abs,

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ENNReal.ofReal |X a| ^ ↑p ∂μ.tilted fun x ↦ t * X x) < ∞
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝⁴ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
this : Measurable fun ω ↦ (X s ω, X t ω)
⊢ Measurable fun ω ↦ (X s ω, X t ω)

Tactic:
Prod.borelSpace.measurable_eq

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝⁴ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
this : Measurable fun ω ↦ (X s ω, X t ω)
⊢ Measurable fun ω ↦ (X s ω, X t ω)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
ω' : Ω'
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) ((κ.map Y) ω')
h_mgf : ∀ (t : ℝ), mgf X ((κ.map Y) ω') t ≤ rexp (↑c * t ^ 2 / 2)
t : ℝ
⊢ mgf (X ∘ Y) (κ ω') = mgf X ((κ.map Y) ω')

Tactic:
ext t

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
ω' : Ω'
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) ((κ.map Y) ω')
h_mgf : ∀ (t : ℝ), mgf X ((κ.map Y) ω') t ≤ rexp (↑c * t ^ 2 / 2)
t✝ t : ℝ
⊢ mgf (X ∘ Y) (κ ω') t = mgf X ((κ.map Y) ω') t
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
this : (1 / 2) ^ n ≤ P (⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)})
⊢ False

Tactic:
by
    refine (by simp : ¬ (1 / 2 : ℝ≥0∞) ^ n ≤ 0) <| this.trans <| nonpos_iff_eq_zero.2 ?_
    rw [measure_eq_zero_iff_ae_notMem]
    filter_upwards [(hσ n).tendsto_top] with ω hTop hmem
    simp_rw [WithTop.tendsto_nhds_top_iff, eventually_atTop] at hTop
    simp only [Set.mem_iInter, Set.mem_ofPred_eq] at hmem
    obtain ⟨N, hN⟩ := hTop (T n)
    specialize hN N le_rfl
    specialize hmem N
    grind

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
⊢ (linearize k G (Action.trivial G X)) g = LinearMap.id

Tactic:
ext (x : X) : 2

Goal state after:
k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
x : X
⊢ ((linearize k G (Action.trivial G X)) g ∘ₗ MonoidAlgebra.lsingle x) 1 = (LinearMap.id ∘ₗ MonoidAlgebra.lsingle x) 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
⊢ integrableExpSet X μ = Set.univ

Tactic:
ext t

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ t ∈ integrableExpSet X μ ↔ t ∈ Set.univ
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 σ
h : ⇑φ = ⇑ψ
⊢ φ = ψ

Tactic:
by
  cases φ; cases ψ
  simpa using h

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

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

Tactic:
by
  ext g v; rfl

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ (fun j ↦ ℙ {ω | X j ω ∈ Set.Ioi ↑j}) = fun j ↦ ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}

Tactic:
ext1 j

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
j : ℕ
⊢ ℙ {ω | X j ω ∈ Set.Ioi ↑j} = ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V✝ : Type u_3
W : Type u_4
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
V : Type u_5
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : ↥S
x✝ : ↥(invariants (MonoidHom.comp ρ S.subtype))
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
⊢ ↑(((MonoidHom.comp (ρ.toInvariants S) S.subtype) g) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
simpa using (hx g)

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case inr
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
· obtain φ : σ.Equiv ρ := Classical.choice inferInstance
    rw [char_iso φ, card_inv_mul_sum_char_mul_char_eq_finrank]
    simp

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
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun x ↦ s.indicator 1 x • c
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, s.indicator (Function.const E c) (X i ω)) atTop
    (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Tactic:
simp only [I, integral_smul_const]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun x ↦ s.indicator 1 x • c
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ x ∈ Finset.range n, s.indicator 1 (X x ω) • c) atTop
    (𝓝 ((∫ (x : Ω), s.indicator 1 (X 0 x) ∂μ) • c))
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 σ
h : ⇑φ = ⇑ψ
⊢ φ = ψ

Tactic:
by
  cases φ; cases ψ
  simpa using h

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
⊢ X.d n ≫ X.d (n + 1) = 0

Tactic:
by
  induction n with
  | zero =>
    ext
    simp [d_succ, ContIntertwiningMap.toContinuousLinearMap_apply, d_zero, hom_sub]
  | succ n ih =>
    rw [d_succ _ (n + 1), Preadditive.comp_sub]
    nth_rw 2 [d_succ]
    rw [Preadditive.sub_comp, ← Functor.map_comp, ih, Functor.map_zero, sub_zero, sub_eq_zero]
    rfl

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ (A.indToCoindAux g) a g₁ = 0

Tactic:
by
  simp [indToCoindAux, dif_neg h]

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
⊢ coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B = 𝟙 (((coinvariantsTensor k H).obj (ind φ A)).obj B)

Tactic:
ext h a b

Goal state after:
k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
a : ↑A
b : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk B).compr₂
                  (ModuleCat.Hom.hom (coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle h)
          1)
        a)
      b =
    (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk B).compr₂
                  (ModuleCat.Hom.hom (𝟙 (((coinvariantsTensor k H).obj (ind φ A)).obj B))) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle h)
          1)
        a)
      b
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
⊢ (Hom.hom (diagonalSuccIsoFree k G n).inv) (single (fun i_1 ↦ i i_1.succ) (MonoidAlgebra.single (i 0) 1)) +
      ∑ x,
        (Hom.hom (diagonalSuccIsoFree k G n).inv)
          (single (x.contractNth (fun x1 x2 ↦ x1 * x2) i) (MonoidAlgebra.single 1 ((-1) ^ (↑x + 1)))) =
    (Hom.hom ((standardComplex k G).d (n + 1) n))
      ((Hom.hom (diagonalSuccIsoFree k G (n + 1)).inv) (single i (MonoidAlgebra.single 1 1)))

Tactic:
have H : ∀ (m : ℕ) (f : Fin m → G) (g : G) (r : k),
        (diagonalSuccIsoFree k G m).inv.hom (single f (MonoidAlgebra.single g r)) =
          MonoidAlgebra.single (g • Fin.partialProd f) r := by
      intro m f g r
      simp only [diagonalSuccIsoFree, diagonalSuccIsoTensorTrivial, Iso.trans_inv, Rep.hom_comp,
        Representation.IntertwiningMap.comp_apply]
      have step1 : (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv)
          (single f (.single g r)) = .single g 1 ⊗ₜ[k] .single f r :=
        Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single f g r
      rw [step1]
      simp only [mkIso_inv, Representation.linearizeOfMulActionIso, Representation.Equiv.mk_symm,
        LinearEquiv.refl_symm, ConcreteCategory.hom_ofHom, Action.tensorObj_V, Action.trivial_V,
        Functor.mapIso_inv, tensor_V, tensor_ρ, Iso.symm_inv, Functor.Monoidal.μIso_hom, μ_hom,
        MonoidalCategory.tensorIso_inv, Representation.linearizeTrivialIso, hom_tensorHom,
        Representation.IntertwiningMap.tensor_apply, Representation.Equiv.coe_toIntertwiningMap,
        Representation.Equiv.mk_apply, LinearEquiv.refl_apply]
      have key₁ := Representation.linearizeMap_single (k := k)
        (Action.diagonalSuccIsoTensorTrivial G m).inv (g, f) ((1 : k) * r)
      have key₂ := Representation.LinearizeMonoidal.μ_apply_single_single (k := k)
        (X := Action.leftRegular G) (Y := Action.trivial G (Fin m → G)) g f 1 r
      exact ((congrArg (fun z => (Representation.linearizeMap
        (Action.diagonalSuccIsoTensorTrivial G m).inv) z) key₂).trans key₁).trans (by simp)

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
H :
  ∀ (m : ℕ) (f : Fin m → G) (g : G) (r : k),
    (Hom.hom (diagonalSuccIsoFree k G m).inv) (single f (MonoidAlgebra.single g r)) =
      MonoidAlgebra.single (g • Fin.partialProd f) r
⊢ (Hom.hom (diagonalSuccIsoFree k G n).inv) (single (fun i_1 ↦ i i_1.succ) (MonoidAlgebra.single (i 0) 1)) +
      ∑ x,
        (Hom.hom (diagonalSuccIsoFree k G n).inv)
          (single (x.contractNth (fun x1 x2 ↦ x1 * x2) i) (MonoidAlgebra.single 1 ((-1) ^ (↑x + 1)))) =
    (Hom.hom ((standardComplex k G).d (n + 1) n))
      ((Hom.hom (diagonalSuccIsoFree k G (n + 1)).inv) (single i (MonoidAlgebra.single 1 1)))