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 ω
⊢ map (fun ω i j ↦ X i j ω) P = map (⇑(MeasurableEquiv.piCurry 𝓧)) (infinitePi fun i ↦ map (fun ω ↦ X i.fst i.snd ω) P)

Tactic:
(iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)).1 h1,

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 ω
⊢ (infinitePi fun i ↦ map (fun ω x ↦ X i x ω) P) =
    map (⇑(MeasurableEquiv.piCurry 𝓧)) (infinitePi fun i ↦ map (fun ω ↦ X i.fst i.snd ω) P)
Module: Mathlib.Probability.Kernel.Category.Stoch

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

Tactic:
rw [SFinKer.Hom.ext_iff] at this

Goal state after:
X Y : Stoch
κ : X ⟶ Y
inst✝ : Deterministic κ
this : (κ.hom ≫ Δ).hom = (Δ ≫ (κ.hom ⊗ₘ κ.hom)).hom
⊢ κ.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₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
rw [condIndep_iff_condIndepSets, condIndepSets_iff]
  · rfl
  · exact hm₁
  · exact hm₂

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

Goal state before:
pp: case refine_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
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] fun ω ↦
          μ[(f ⁻¹' s).indicator fun ω ↦ 1 | m'] ω * μ[(g ⁻¹' t).indicator fun ω ↦ 1 | m'] ω
s t : Set Ω
⊢ MeasurableSet s →
    MeasurableSet t →
      μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
rintro ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Goal state after:
case refine_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
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] fun ω ↦
          μ[(f ⁻¹' s).indicator fun ω ↦ 1 | m'] ω * μ[(g ⁻¹' t).indicator fun ω ↦ 1 | m'] ω
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
    μ[(f ⁻¹' s).indicator fun ω ↦ 1 | m'] * μ[(g ⁻¹' t).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a = ∑' (a : ↑p.support), (p ↑a).toReal • f ↑a

Tactic:
by
    congr with x; congr 2
    apply PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

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 * ↑ε))
⊢ (κ ω').real {ω | ↑ε ≤ X ω} = 0

Tactic:
have hl : Filter.Tendsto (fun t ↦ rexp (-(t * ε))) Filter.atTop (𝓝 0) := by
      apply tendsto_exp_neg_atTop_nhds_zero.comp
      exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)

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 * ↑ε))
hl : Filter.Tendsto (fun t ↦ rexp (-(t * ↑ε))) Filter.atTop (𝓝 0)
⊢ (κ ω').real {ω | ↑ε ≤ X ω} = 0
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
⊢ stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n) =
    stoppedProcess
      (fun i ↦
        {ω | ⊥ < hqX.localSeq n ω}.indicator
          (stoppedProcess (fun i ↦ {ω | ⊥ < hpX.localSeq n ω}.indicator (X i)) (hpX.localSeq n) i))
      (hqX.localSeq n)

Tactic:
ext i ω

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 ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i)) ((hpX.localSeq ⊓ hqX.localSeq) n)
      i ω =
    stoppedProcess
      (fun i ↦
        {ω | ⊥ < hqX.localSeq n ω}.indicator
          (stoppedProcess (fun i ↦ {ω | ⊥ < hpX.localSeq n ω}.indicator (X i)) (hpX.localSeq n) i))
      (hqX.localSeq n) i ω
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))
n : ℕ
⊢ (fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ τ n ω) i)) = fun i ↦
    {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n) i)

Tactic:
ext i ω

Goal state after:
ι : 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))
n : ℕ
i : ι
ω : Ω
⊢ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ τ n ω) i) ω =
    {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n) i) ω
Module: Mathlib.Probability.StrongLaw

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

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)

Tactic:
← integral_indicator M

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

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case inl
α : 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 : 0 ≤ A
⊢ ∫ (y : ℝ), (Set.Ioc 0 A).indicator id y ^ n ∂Measure.map f μ = ∫ (x : ℝ) in Set.Ioc 0 A, x ^ n ∂Measure.map f μ

pp: case inl
α : 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 : 0 ≤ A
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc 0 A).indicator id z ^ n) (Measure.map f μ)

Tactic:
← integral_indicator M

Goal state after:
case inl
α : 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 : 0 ≤ A
⊢ ∫ (y : ℝ), (Set.Ioc 0 A).indicator id y ^ n ∂Measure.map f μ =
    ∫ (x : ℝ), (Set.Ioc 0 A).indicator (fun x ↦ x ^ n) x ∂Measure.map f μ

case inl
α : 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 : 0 ≤ A
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc 0 A).indicator id z ^ n) (Measure.map f μ)
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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
⊢ (stoppedProcess (fun i ↦ {ω | ⊥ < min (hL.localSeq n ω) (τ n (nk n) ω)}.indicator (X i)) fun ω ↦
      min (hL.localSeq n ω) (τ n (nk n) ω)) =
    stoppedProcess
      (fun i ↦
        {ω | ⊥ < τ n (nk n) ω}.indicator
          (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
      (τ n (nk n))

Tactic:
ext i ω

Goal state after:
ι : 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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω : Ω
⊢ stoppedProcess (fun i ↦ {ω | ⊥ < min (hL.localSeq n ω) (τ n (nk n) ω)}.indicator (X i))
      (fun ω ↦ min (hL.localSeq n ω) (τ n (nk n) ω)) i ω =
    stoppedProcess
      (fun i ↦
        {ω | ⊥ < τ n (nk n) ω}.indicator
          (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
      (τ n (nk n)) i ω
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
x : X
⊢ ((linearize k G (Action.trivial G X)) g ∘ₗ MonoidAlgebra.lsingle x) 1 = (LinearMap.id ∘ₗ MonoidAlgebra.lsingle x) 1

Tactic:
rw [LinearMap.comp_apply, LinearMap.id_comp, MonoidAlgebra.lsingle_apply, linearize_single]

Goal state after:
k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
x : X
⊢ MonoidAlgebra.single ((ConcreteCategory.hom ((Action.trivial G X).ρ g)) x) 1 = MonoidAlgebra.single x 1
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✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
this : (ρ g ∘ₗ (↑φ.symm).toLinearMap) w = ((↑φ.symm).toLinearMap ∘ₗ σ g) w
⊢ (φ.toLinearEquiv.conj (ρ g)) w = (σ g) w

Tactic:
simp only [LinearMap.coe_comp, coe_toLinearMap, Function.comp_apply, LinearEquiv.conj_apply_apply,
    coe_symm, toLinearEquiv_apply, coe_toIntertwiningMap] at this ⊢

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
this : (ρ g) (φ.symm w) = φ.symm ((σ g) w)
⊢ φ ((ρ g) (φ.symm w)) = (σ g) w
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : FiniteDimensional k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g = ↑(finrank k ↥ρ.invariants)

Tactic:
by
  have : Invertible (Fintype.card G : k) := by rw [Fintype.card_eq_nat_card]; assumption
  rw [← (isProj_averageMap ρ).trace]
  simp [character, GroupAlgebra.average, _root_.map_sum]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁸ : Field k
G : Type u_2
inst✝⁷ : Finite G
inst✝⁶ : NeZero ↑(Nat.card G)
inst✝⁵ : Group G
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module k[G] V
W : Type u_4
inst✝² : AddCommGroup W
inst✝¹ : Module k[G] W
inst✝ : AddGroup G
⊢ NeZero ↑(Nat.card (Multiplicative G))

Tactic:
rwa [Nat.card_congr Multiplicative.toAdd]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ cechNerveTerminalFrom G ≅ classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)

Tactic:
by
  refine NatIso.ofComponents (fun _ => Types.productIso _) fun _ => ?_
  ext : 2
  exact Matrix.ext fun _ _ => Pi.lift_π_apply (f := fun _ ↦ G) _ _ _

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
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
⊢ (Algebra.norm K) x⁻¹ = 1

Tactic:
simp [Algebra.norm_inv, hx]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ModuleCat.Hom.hom ((cochainsIso₁ X.X₃).inv ≫ (inhomogeneousCochains X.X₃).d 1 (1 + 1))) ⇑z = 0

Tactic:
eq_d₁₂_comp_inv

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₁₂ X.X₃ ≫ (cochainsIso₂ X.X₃).inv)) ⇑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g : Fin (1 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ModuleCat.Hom.hom ((cochainsIso₁ X.X₂).inv ≫ (inhomogeneousCochains X.X₂).d 1 (1 + 1))) y g

Tactic:
eq_d₁₂_comp_inv

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g : Fin (1 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ModuleCat.Hom.hom (d₁₂ X.X₂ ≫ (cochainsIso₂ X.X₂).inv)) y g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ⇑x ∈ coboundaries₂ A

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv
    (shortComplexH2 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousCochains A).sc 2).leftHomologyIso.hom

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
h :
  (shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso.hom
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ⇑x ∈ coboundaries₂ A
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Nontrivial k
⊢ Function.Injective ⇑(equivHom k G)

Tactic:
by
  intro s t h
  classical
  apply_fun (fun x ↦ (x.hom.hom.app rightFDRep).hom (single t 1) 1) at h
  simp_all [single_apply]

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
⊢ rename id = AlgHom.id R (MvPowerSeries σ R)

Tactic:
ext _ y

Goal state after:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x✝ : MvPowerSeries σ R
y : σ →₀ ℕ
⊢ (coeff y) ((rename id) x✝) = (coeff y) ((AlgHom.id R (MvPowerSeries σ R)) x✝)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ 𝓝 0 = 𝓝 0

Tactic:
ext s
      let := Ideal.adic_basis J
      rw [J.hasBasis_nhds_zero_adic.mem_iff]
      constructor <;> intro H
      · rcases H₂ s H with ⟨n, h⟩
        exact ⟨n, trivial, h⟩
      · rcases H with ⟨n, -, hn⟩
        rw [mem_nhds_iff]
        exact ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩

Goal state after: