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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this✝² : IsProbabilityMeasure P
this✝¹ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (map (X i j) P)
this✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun ω x ↦ X i x ω) P)
this : (⇑(MeasurableEquiv.piCurry 𝓧) ∘ fun ω p ↦ X p.fst p.snd ω) = fun ω i j ↦ X i j ω
i : ι
⊢ map (fun ω x ↦ X i x ω) P = infinitePi fun j ↦ map (X i j) P

Tactic:
(iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)).1 (h2 i)

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this✝² : IsProbabilityMeasure P
this✝¹ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (map (X i j) P)
this✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun ω x ↦ X i x ω) P)
this : (⇑(MeasurableEquiv.piCurry 𝓧) ∘ fun ω p ↦ X p.fst p.snd ω) = fun ω i j ↦ X i j ω
i : ι
⊢ (infinitePi fun i_1 ↦ map (X i i_1) P) = infinitePi fun j ↦ map (X i j) P
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case neg.refine_1
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
⊢ ‖∫ (x : Ω), f x ∂μ[|s]‖ₑ = 0 ∨ (μ.restrict s) t < ∞

Tactic:
exact Or.inr <| measure_lt_top (μ.restrict s) t

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
⊢ map (fun ω ↦ (Z ω, fun a ↦ Y a ω)) P = (map Z P).prod (map (fun c a ↦ Y a c) P)

Tactic:
refine eq_prod_of_integral_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Goal state after:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ ∫ (p : G × ((j : T) → F j)), f p.1 * ∏ j, (g j) (p.2 j) ∂map (fun ω ↦ (Z ω, fun a ↦ Y a ω)) P =
    (∫ (z : G), f z ∂map Z P) * ∫ (y : (j : T) → F j), ∏ j, (g j) (y j) ∂map (fun c a ↦ Y a c) P
Module: Mathlib.Probability.Kernel.Category.Stoch

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

Tactic:
have : IsDeterministic (κ ≫ η).hom.hom := inferInstance

Goal state after:
X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ Z✝ : Stoch
κ : X✝ ⟶ Y✝
η : Y✝ ⟶ Z✝
x✝ : Deterministic (κ ≫ η)
this : IsDeterministic (κ ≫ η).hom.hom
⊢ η.hom.hom ∥ₖ Kernel.id ∘ₖ copy Y✝.obj.carrier ∘ₖ κ.hom.hom =
    η.hom.hom ∘ₖ κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X✝.obj.carrier
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ c * ∫⁻ (a : X), B.indicator 1 a * A.indicator 1 a ∂π x₀ = B.indicator 1 x₀ * (c * ∫⁻ (a : X), A.indicator 1 a ∂π x₀)

pp: case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable (A.indicator 1)

pp: case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ B.indicator 1 x * A.indicator 1 x

Tactic:
hπ.lintegral_indicator_mul_indicator h𝓑𝓧 hA hB,

Goal state after:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ c * (B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂π x₀) =
    B.indicator 1 x₀ * (c * ∫⁻ (a : X), A.indicator 1 a ∂π x₀)

case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable (A.indicator 1)

case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ B.indicator 1 x * A.indicator 1 x
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
⊢ CondIndepSets m' hm' {s} {t} μ ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
condIndepSets_iff _ _ _ _ ?_ ?_

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
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ {s} →
        t2 ∈ {t} →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']) ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ s_1 ∈ {s}, MeasurableSet s_1

Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ s ∈ {t}, MeasurableSet s
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case hs1
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
exact hm₁

Goal state after:
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
hξ : f a ξ ≤ x
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))
⊢ (fun x ↦ ↑ξ) ≤ᶠ[𝓝[>] x] g

Tactic:
refine eventually_nhdsWithin_of_forall fun y hy ↦ ?_
      by_contra! h
      simp only [sSup_le_iff, f] at hξ
      specialize hξ y h
      grind

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ StronglyMeasurable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ))

Tactic:
refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)

Goal state after:
case refine_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ StronglyMeasurable (stoppedValue (fun n ↦ f n) τ)
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
hX : IsAEKolmogorovProcess X P p q M
s t : T
ω : Ω
hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω
hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω
⊢ edist (X s ω) (X t ω) = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)

Tactic:
by simp [hω₁, hω₂]

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 : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
⊢ rexp (-(ε / ↑c) * ε + ↑c * (ε / ↑c) ^ 2 / 2) = rexp (-ε ^ 2 / (2 * ↑c))

Tactic:
by congr; field

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
x₂ : W
hx₂ : x₂ ∈ ρ₂.toSubmodule
⊢ (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
exact Submodule.mem_sup.mpr
        ⟨ρ g x₁, ρ₁.apply_mem_toSubmodule g hx₁, ρ g x₂, ρ₂.apply_mem_toSubmodule g hx₂, rfl⟩

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 : ι
ω : Ω
⊢ {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω}.indicator (stoppedProcess X (hqX.localSeq n ⊓ hpX.localSeq n) i) ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω

Tactic:
← stoppedProcess_stoppedProcess,

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 : ι
ω : Ω
⊢ {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω}.indicator
      (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i) ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case single
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ MonoidAlgebra.single g (a * 1) • m ∈ σ.toSubmodule.carrier

Tactic:
← smul_eq_mul,

Goal state after:
case single
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ MonoidAlgebra.single g (a • 1) • m ∈ σ.toSubmodule.carrier
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
⊢ Locally p 𝓕 X P

Tactic:
by
  refine ⟨_, hτ.isLocalizingSequence_biInf, fun n ↦ ?_⟩
  rw [stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess_of_le_right
    (τ := fun ω ↦ τ n ω) (fun _ ↦ (iInf_le _ n).trans <| iInf_le _ le_rfl),
    ← stoppedProcess_indicator_comm']
  convert!
    hp _ (hpτ n) (fun ω ↦ ⨅ j ≥ n, τ j ω) <| hτ.isLocalizingSequence_biInf.isStoppingTime n using 2
  ext i ω
  rw [stoppedProcess_indicator_comm', Set.indicator_indicator]
  congr with ω
  exact ⟨fun h ↦ ⟨h, lt_of_lt_of_le h <| (iInf_le _ n).trans (iInf_le _ le_rfl)⟩, fun h ↦ h.1⟩

Goal state after:
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)})
ω : Ω
hmem : ω ∈ ⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)}
hTop : ∀ (i : ι), ∃ a, ∀ (b : ℕ), a ≤ b → ↑i < σ n b ω
⊢ False

Tactic:
simp only [Set.mem_iInter, Set.mem_ofPred_eq] at hmem

Goal state after:
ι : 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)})
ω : Ω
hTop : ∀ (i : ι), ∃ a, ∀ (b : ℕ), a ≤ b → ↑i < σ n b ω
hmem : ∀ (i : ℕ), σ n i ω < min (τ n ω) ↑(T n)
⊢ False
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ ∫ (y : ℝ), (Set.Ioc 0 A).indicator id y ^ n ∂Measure.map f μ =
    -∫ (x : ℝ), (Set.Ioc A 0).indicator (fun x ↦ x ^ n) x ∂Measure.map f μ

Tactic:
simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow hn, Set.indicator_empty, integral_zero,
        zero_eq_neg]
      apply integral_eq_zero_of_ae
      have : ∀ᵐ x ∂Measure.map f μ, (0 : ℝ) ≤ x :=
        (ae_map_iff hf.aemeasurable measurableSet_Ici).2 (Eventually.of_forall h'f)
      filter_upwards [this] with x hx
      simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp]
      intro _ h''x
      have : x = 0 := by linarith
      simp [this, zero_pow hn]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
⊢ S.ShortExact

Tactic:
have h₁ := h.1

Goal state after:
case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
h₁ : (S.map (resFunctor φ)).Exact
⊢ S.ShortExact
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have posm : Measurable pos := measurable_id'.max measurable_const

Goal state after:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ Hom.hom
      (ofHom (δ (X ⊗ Y) Z) ≫
        ofHom (δ X Y) ▷ (linearization k G).obj Z ≫
          (α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom) =
    Hom.hom ((linearization k G).map (α_ X Y Z).hom ≫ ofHom (δ X (Y ⊗ Z)) ≫ (linearization k G).obj X ◁ ofHom (δ Y Z))

Tactic:
simpa using assoc_comp_δ X Y Z (k := k)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (compForgetAugmented G).ExtraDegeneracy

Tactic:
refine
    ExtraDegeneracy.ofIso (?_ : (Arrow.mk <| terminal.from G).augmentedCechNerve ≅ _)
      (extraDegeneracyAugmentedCechNerve G)
  exact
    Comma.isoMk (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)
      (Iso.refl _) (by ext : 1; exact IsTerminal.hom_ext terminalIsTerminal _ _)

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

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (MonoidAlgebra.single c (r * 1)) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r * 1 * (-1) ^ ↑p)

Tactic:
← smul_eq_mul,

Goal state after:
k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (MonoidAlgebra.single c (r • 1)) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r • 1 * (-1) ^ ↑p)
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w✝¹ → R
H : ∑ x, s x * p x + (∑ i, s i * r i) * a = y
⊢ a * ∑ k, s k * r k ∈ span (Set.range fun a_1 ↦ a • i a_1)

Tactic:
← smul_eq_mul,

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w✝¹ → R
H : ∑ x, s x * p x + (∑ i, s i * r i) * a = y
⊢ a • ∑ k, s k * r k ∈ span (Set.range fun a_1 ↦ a • i a_1)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ single (h, 1) ((A.ρ g⁻¹) a) - single (g * h, 1) a ∈ boundaries₂ A

Tactic:
use single (g, h, 1) a

Goal state after:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ (ModuleCat.Hom.hom (d₃₂ A)) (single (g, h, 1) a) = single (h, 1) ((A.ρ g⁻¹) a) - single (g * h, 1) a
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i N : ℕ
hN : ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i
⊢ f i - L ∈ I ^ i

Tactic:
simpa using Ideal.add_mem _ (hN (max i N) le_sup_right) (hf (le_max_left i N))

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ (degree x + 1) * ⊤

Tactic:
← smul_eq_mul,

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤