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

Goal state before:
pp: case a
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (fun ω ↦ ω i) ⟂ᵢ[infinitePi P] fun ω ↦ ω j

pp: ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (map (fun ω ↦ ω i) (infinitePi P)).prod (map (fun ω ↦ ω j) (infinitePi P)) = (P i).prod (P j)

pp: case hf
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω i) (infinitePi P)

pp: case hg
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω j) (infinitePi P)

Tactic:
· exact iIndepFun_infinitePi (X := fun x ω ↦ ω) (by fun_prop) |>.indepFun hij

Goal state after:
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (map (fun ω ↦ ω i) (infinitePi P)).prod (map (fun ω ↦ ω j) (infinitePi P)) = (P i).prod (P j)

case hf
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω i) (infinitePi P)

case hg
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω j) (infinitePi P)
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x ↦ μ[|s].real t

Tactic:
rw [← integral_indicator_one ht]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x ↦ ∫ (x : Ω), t.indicator 1 x ∂μ[|s]
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
inst✝ : Deterministic κ
this : copy Y.obj.carrier ∘ₖ κ.hom.hom = Kernel.id ∥ₖ κ.hom.hom ∘ₖ (κ.hom.hom ∥ₖ Kernel.id) ∘ₖ copy X.obj.carrier
⊢ κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier = copy Y.obj.carrier ∘ₖ κ.hom.hom

Tactic:
rw [id_parallelComp_comp_parallelComp_id] at this

Goal state after:
X Y : Stoch
κ : X ⟶ Y
inst✝ : Deterministic κ
this : copy Y.obj.carrier ∘ₖ κ.hom.hom = κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier
⊢ κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier = copy Y.obj.carrier ∘ₖ κ.hom.hom
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h' : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
⊢ (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω →
    ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t →
      μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω

Tactic:
hst_eq

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h' : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
⊢ ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t →
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
hs : s ∈ s1
ht : t ∈ s2
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
⊢ (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω →
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω →
      ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t

Tactic:
hst_eq

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
hs : s ∈ s1
ht : t ∈ s2
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω →
    ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' ∈ {s}
⊢ MeasurableSet s'

Tactic:
rw [Set.mem_singleton_iff] at hs'

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = s
⊢ MeasurableSet s'
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' ∈ {t}
⊢ MeasurableSet s'

Tactic:
rw [Set.mem_singleton_iff] at hs'

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = t
⊢ MeasurableSet s'
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 μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
⊢ CondIndepFun m' hm' X Y μ

Tactic:
condIndepFun_iff _ hm' _ _ (hX.mono hm' le_rfl) hY

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
⊢ ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']
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 μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(X ⁻¹' s ∩ Y ⁻¹' t).indicator 1 | m'] =ᵐ[μ] μ[(X ⁻¹' s).indicator 1 | m'] * μ[(Y ⁻¹' t).indicator 1 | m']

Tactic:
Set.inter_indicator_one

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(X ⁻¹' s).indicator 1 * (Y ⁻¹' t).indicator 1 | m'] =ᵐ[μ]
    μ[(X ⁻¹' s).indicator 1 | m'] * μ[(Y ⁻¹' t).indicator 1 | m']
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case neg.refine_2
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
y : ↑I
hy : y ∈ Ioi x
h : g y < ↑ξ
hξ : ∀ b ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}, b ≤ x
⊢ False

Tactic:
specialize hξ y h

Goal state after:
case neg.refine_2
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
y : ↑I
hy : y ∈ Ioi x
h : g y < ↑ξ
hξ : y ≤ x
⊢ False
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Tendsto (fun A ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ |f a|

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x ↦ |f x|) μ

case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ truncation f n a) atTop (𝓝 (f a))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ truncation f n a) atTop (𝓝 (f a))

Tactic:
· filter_upwards with x
    apply tendsto_const_nhds.congr' _
    filter_upwards [Ioi_mem_atTop (abs (f x))] with A hA
    exact (truncation_eq_self hA).symm

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 i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Tendsto (fun N ↦ ℙ {ω | X ω ∈ Set.Ioc ↑i ↑N}) atTop (𝓝 (ℙ (⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N})))

Tactic:
apply tendsto_measure_iUnion_atTop

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Monotone fun N ↦ {ω | X ω ∈ Set.Ioc ↑i ↑N}
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
φ✝ φ : ρ.Equiv σ
g : G
⊢ ↑φ.toLinearEquiv.symm ∘ₗ σ g = ρ g ∘ₗ ↑φ.toLinearEquiv.symm

Tactic:
← cancel_left φ.toLinearEquiv.injective,

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
φ✝ φ : ρ.Equiv σ
g : G
⊢ ↑φ.toLinearEquiv ∘ₗ ↑φ.toLinearEquiv.symm ∘ₗ σ g = ↑φ.toLinearEquiv ∘ₗ ρ g ∘ₗ ↑φ.toLinearEquiv.symm
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hX
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ MemLp (S (u i)) 2 ℙ

pp: case h.hc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 0 < ↑(u i) * ε

Tactic:
· exact memLp_finsetSum' _ fun j _ => (hident j).aestronglyMeasurable_fst.memLp_truncation

Goal state after:
case h.hc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 0 < ↑(u i) * ε
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Tactic:
nth_rw 1 [← h]

Goal state after:
case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ (Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹) ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f → f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

pp: case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
⊢ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f → Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f

Tactic:
· intro h
    nth_rw 1 [← h]
    rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]

Goal state after:
case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
⊢ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f → Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
· have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
      rw [ae_all_iff]
      intro i
      exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
    filter_upwards [I] with ω hω
    simpa [hω] using (integral_eq_zero_of_ae h).symm

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
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
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
h : H
f : C(H, V)
hf : f ∈ coindV φ π
⊢ f.comp (ContinuousMap.mulRight h) ∈ coindV φ π

Tactic:
simp [mul_assoc, hf _]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case zero
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ QuasiIsoAt
    ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
      ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)
    0

Tactic:
rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros' _ rfl rfl rfl]

Goal state after:
case zero
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
        X₂ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
        f :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
              ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
                ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
          ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
            ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂