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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
⊢ (p a * ∑' (b : β), if b ∈ s then if h : p a = 0 then 0 else (f a h) b else 0) =
    p a * if h : p a = 0 then 0 else ∑' (b : β), if b ∈ s then (f a h) b else 0

Tactic:
split_ifs with ha

Goal state after:
case pos
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : p a = 0
⊢ (p a * ∑' (b : β), if b ∈ s then 0 else 0) = p a * 0

case neg
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : ¬p a = 0
⊢ (p a * ∑' (b : β), if b ∈ s then (f a ha) b else 0) = p a * ∑' (b : β), if b ∈ s then (f a ha) b else 0
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:

Tactic:
0 = (0 : Measure E) Set.univ := rfl
    _ = _ := by rw [hu, Measure.smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]

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

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
⊢ μ[|s] ≪ μ

Tactic:
exact ProbabilityTheory.cond_absolutelyContinuous

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∏ i, (map (s.restrict X i) P) (t ↑i) = ∏ i ∈ s, (map (X i) P) (t i)

pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P

Tactic:
· simp only [Finset.restrict]
      rw [s.prod_coe_sort fun i ↦ P.map (X i) (t i)]

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) = map (fun ω ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i))

Tactic:
change _ = map (((fun f ↦ f j) ∘ (fun f ↦ f i)) ∘ (fun ω i j ↦ X i j (ω i j)))
      (infinitePi fun i ↦ infinitePi (μ i))

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) =
    map (((fun f ↦ f j) ∘ fun f ↦ f i) ∘ fun ω i j ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i))
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ μ t = 0 ∨ μ t = 1

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
    using! Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop h_le h_indep ht_tail

Goal state after:
Module: Mathlib.Probability.Kernel.Irreducible

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst✝ : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : φ s > 0
a : α
⊢ ∃ n, ((Kernel.id ^ n) a) s > 0

Tactic:
by
    use 1;
    have ha : a ∈ s :=
      Subsingleton.mem_iff_nonempty.mpr
        <| MeasureTheory.nonempty_of_measure_ne_zero (μ := φ) (ne_of_lt hsp).symm
    simp [id_apply, ha]

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.id.map Prod.snd ∘ₖ Kernel.id.map f₁ = Kernel.id

Tactic:
rw [Kernel.id_map hf₂, Kernel.deterministic_comp_eq_map hf₂, Kernel.id_map hf₁,
        Kernel.deterministic_map hf₁ hf₂]

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.deterministic (Prod.snd ∘ f₁) ⋯ = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.id.map Prod.fst ∘ₖ Kernel.id.map f₁ = Kernel.id

Tactic:
rw [Kernel.id_map hf₂, Kernel.deterministic_comp_eq_map hf₂, Kernel.id_map hf₁,
        Kernel.deterministic_map hf₁ hf₂]

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.deterministic (Prod.fst ∘ f₁) ⋯ = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ X ⊗ Y ≅ Y ⊗ X

Tactic:
refine ⟨⟨Kernel.swap _ _, by rw [Kernel.swap]; infer_instance⟩,
      ⟨Kernel.swap _ _, by rw [Kernel.swap]; infer_instance⟩, ?_, ?_⟩
    · ext : 1; simp
    · ext : 1; simp

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

Goal state before:
pp: case e'_2
Ω : 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
⊢ Measure.map (Prod.map id fun ω ↦ (f ω, g ω)) (Measure.map Function.diag μ) = Measure.map (fun ω ↦ (ω, f ω, g ω)) μ

Tactic:
exact Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
⊢ Filter.Tendsto (fun t ↦ rexp (-(t * ↑ε))) Filter.atTop (𝓝 0)

Tactic:
apply tendsto_exp_neg_atTop_nhds_zero.comp

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
⊢ Filter.Tendsto (fun t ↦ t * ↑ε) Filter.atTop Filter.atTop
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
⊢ X =ᵐ[⇑κ ∘ₘ ν] fun ω ↦ X ω + Y ω

Tactic:
filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hY] with ω hY0 using by simp [hY0]

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess
      (fun i ↦ {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω}.indicator (stoppedProcess X (hpX.localSeq n) i))
      (hqX.localSeq n) i ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω

Tactic:
Set.ofPred_and,

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess
      (fun i ↦
        ({a | ⊥ < hpX.localSeq n a} ∩ {a | ⊥ < hqX.localSeq n a}).indicator (stoppedProcess X (hpX.localSeq n) i))
      (hqX.localSeq n) i ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos.inr.refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (fun ω ↦ rexp (t * X ω)) (↑2) (⇑κ ∘ₘ ν)
⊢ MemLp (fun ω ↦ rexp (t * X ω.1)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
simp only [ENNReal.coe_ofNat] at h

Goal state after:
case pos.inr.refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (fun ω ↦ rexp (t * X ω)) 2 (⇑κ ∘ₘ ν)
⊢ MemLp (fun ω ↦ rexp (t * X ω.1)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ =
    ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∑ k ∈ range j, ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
by
      congr 1 with j
      congr 1
      rw [intervalIntegral.sum_integral_adjacent_intervals]
      · norm_cast
      intro k _
      exact (continuous_id.pow _).intervalIntegrable _ _

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
l1 : k[X.V]
l2 : k[Y.V]
xy : (X ⊗ Y).V
⊢ ((μ X Y) (l1 ⊗ₜ[k] l2)).coeff xy = l1.coeff xy.1 * l2.coeff xy.2

Tactic:
simp [← toLinearMap_apply, types_tensorObj_def, finsuppTensorFinsupp'_apply_apply _]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ k ∈ range K, (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤
    ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
by
      gcongr with k
      · refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _
        simp
      · apply sum_Ioo_inv_sq_le

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
Y : Ω → ℝ
h' : X =ᵐ[μ] Y
⊢ HasSubgaussianMGF Y c μ

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h ⊢
  apply h.congr
  simpa

Goal state after:
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝³ : Monoid G
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsIrreducible ↔ IsSimpleModule k[G] ρ.asModule

Tactic:
rw [isSimpleModule_iff]

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
inst✝³ : Monoid G
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsIrreducible ↔ IsSimpleOrder (Submodule k[G] ρ.asModule)
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ IsSimpleModule k[G] M ↔ (ofModule M).IsIrreducible

Tactic:
rw [isSimpleModule_iff]

Goal state after:
G : Type u_1
k : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ IsSimpleOrder (Submodule k[G] M) ↔ (ofModule M).IsIrreducible
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
g : G
⊢ (V ⊗ W).character g = (V.character * W.character) g

Tactic:
convert! trace_tensorProduct' (V.ρ g) (W.ρ g)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have A : ∀ᵐ ω ∂μ, ∀ k,
      Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, Y k i ω)) atTop (𝓝 μ[Y k 0]) :=
    ae_all_iff.2 (fun k ↦ strong_law_ae_simpleFunc_comp X h'.measurable hindep hident (φ k))

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
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
⊢ ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < a'

Tactic:
intro ε

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
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
⊢ ε > 0 → ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < ε
Module: Mathlib.Probability.StrongLaw

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

Tactic:
gcongr
      exact hn.le

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
x✝ : (fun π ↦ ⇑π.toMonoidHom) π₁ = (fun π ↦ ⇑π.toMonoidHom) π₂
⊢ π₁ = π₂

Tactic:
by cases π₁; cases π₂; simp_all

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
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
x✝ : (QuotientGroup.rightRel S) (↑s * g₁) g
s₁ : ↥S
hs₁ : (fun m ↦ m • g) s₁ = ↑s * g₁
⊢ (fun m ↦ m • g) (s⁻¹ * s₁) = g₁

Tactic:
by simp_all [S.1.smul_def, mul_assoc]

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
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
x✝ : (QuotientGroup.rightRel S) g₂ (↑s * g₁)
s₁ : ↥S
hs₁ : (fun m ↦ m • (↑s * g₁)) s₁ = g₂
⊢ (fun m ↦ m • g₁) (s₁ * s) = g₂

Tactic:
by simp_all [S.1.smul_def, mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
⊢ ∃ y, ↑y / g ↑y = x

Tactic:
suffices H : ∀ x, Algebra.norm K x = 1 → ∃ y : Lˣ, g y / y = x by
    have hxinv : Algebra.norm K x⁻¹ = 1 := by simp [Algebra.norm_inv, hx]
    obtain ⟨y, hy⟩ := H _ hxinv
    use y
    rw [IsUnit.div_eq_iff y.isUnit] at hy
    rw [hy]
    field_simp

Goal state after:
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
⊢ ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x