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

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

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h✝ : b ∈ s
⊢ ∑' (a : α), p a * (f a) b = ∑' (a : α), p a * (f a) b

case neg
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h✝ : b ∉ s
⊢ 0 = ∑' (a : α), p a * 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
⊢ (if b ∈ s then (f a) b else 0) = if b ∈ s then (f a) b else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∈ s
⊢ (f a) b = (f a) b

case neg
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∉ s
⊢ 0 = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false
p : ℝ≥0
h : p ≤ 1
⊢ ¬↑1 - ↑p = 0 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}

Tactic:
ENNReal.coe_one,

Goal state after:
case false
p : ℝ≥0
h : p ≤ 1
⊢ ¬1 - ↑p = 0 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}
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
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ 0 Set.univ = 1

Tactic:
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.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ Integrable (fun ω ↦ ((condExpKernel μ m) ω).real s) μ

Tactic:
nontriviality Ω
  rw [condExpKernel_eq]
  exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
⊢ f (if ω ∈ A then 1 ω else 0) * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω

Tactic:
split_ifs

Goal state after:
case pos
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
h✝ : ω ∈ A
⊢ f (1 ω) * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω

case neg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
h✝ : ω ∉ A
⊢ f 0 * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
ω : Ω
⊢ f (if ω ∈ A then 1 ω else 0) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω

Tactic:
split_ifs

Goal state after:
case pos
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
ω : Ω
h✝ : ω ∈ A
⊢ f (1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω

case neg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
ω : Ω
h✝ : ω ∉ A
⊢ f 0 = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)

Tactic:
tilted_apply_eq_ofReal_integral _ s,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : 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
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
⊢ μ[stoppedValue f τ | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
h1

Goal state after:
Ω : 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
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = 1 ^ n

Tactic:
one_pow

Goal state after:
case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = 1
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 κ ν
ε : ℝ
ω' : Ω'
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) →
    (∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')) →
      IsFiniteMeasure (κ ω') → ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)

Tactic:
h1

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ (∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')) →
    IsFiniteMeasure (κ ω') → ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
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 ↦ t * ↑ε) Filter.atTop Filter.atTop

Tactic:
exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)

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 κ ν
ω' : Ω'
⊢ (κ ω') {ω | 0 < (-X) ω} = 0 → (κ ω') {ω | 0 < X ω} = 0 → X =ᵐ[κ ω'] 0

Tactic:
h1

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h1 : (κ ω') {ω | 0 < (-X) ω} = 0
⊢ (κ ω') {ω | 0 < X ω} = 0 → X =ᵐ[κ ω'] 0
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |f x|

case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
exact abs_truncation_le_abs_self _ _ _

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h₂
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
⊢ ∫ (x : ℝ) in 0..↑N, 1 ∂ρ ≤ 1

Tactic:
intervalIntegral.integral_of_le (Nat.cast_nonneg _)

Goal state after:
case h₂
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∫ (x : ℝ) in Set.Ioc 0 ↑N, 1 ∂ρ ≤ 1
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝⁶ : Monoid G
V : Type v'
inst✝⁵ : AddCommMonoid V
W : Type w'
inst✝⁴ : AddCommMonoid W
k : Type u
inst✝³ : CommSemiring k
inst✝² : Module k V
inst✝¹ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst✝ : DecidableEq α
v : V
f : α →₀ W
i : α
⊢ ((σ.finsuppTensorRight ρ α) (v ⊗ₜ[k] f)) i = v ⊗ₜ[k] f i

Tactic:
simp +contextual [finsuppTensorRight_apply_tmul, Finsupp.sum_apply, Finsupp.single_apply]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat k[G]
f : X✝ ⟶ Y✝
g : G
⊢ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ (Representation.ofModule ↑X✝) g =
    (Representation.ofModule ↑Y✝) g ∘ₗ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ }

Tactic:
ext; apply f.hom.map_smul

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
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
⊢ ∀ᵐ (a : Ω) ∂μ,
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) a‖) / ↑n) atTop
      (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))

Tactic:
let G : ℕ → E → ℝ := fun k x ↦ ‖x - φ k x‖

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 ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun k x ↦ ‖x - (φ k) x‖
⊢ ∀ᵐ (a : Ω) ∂μ,
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) a‖) / ↑n) atTop
      (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
hγ : ∀ (s : ↥S) (g : G), γ (↑s * g) = s * γ g
x : G → ↑X := fun g ↦ (X.ρ (γ g)) (s (↑y (i (Quotient.mk' g))))
⊢ ∃ a, (Hom.hom ((coindFunctor k S.subtype).map f)) a = y

Tactic:
refine ⟨⟨x, fun _ _ => ?_⟩, Subtype.ext <| funext fun g => ?_⟩

Goal state after:
case refine_1
k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
hγ : ∀ (s : ↥S) (g : G), γ (↑s * g) = s * γ g
x : G → ↑X := fun g ↦ (X.ρ (γ g)) (s (↑y (i (Quotient.mk' g))))
x✝¹ : ↥S
x✝ : G
⊢ x (S.subtype x✝¹ * x✝) = (X.ρ x✝¹) (x x✝)

case refine_2
k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
hγ : ∀ (s : ↥S) (g : G), γ (↑s * g) = s * γ g
x : G → ↑X := fun g ↦ (X.ρ (γ g)) (s (↑y (i (Quotient.mk' g))))
g : G
⊢ ↑((Hom.hom ((coindFunctor k S.subtype).map f)) ⟨x, ⋯⟩) g = ↑y g
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
⊢ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ = 0

Tactic:
simp only [integral_eq_zero_of_ae h, sub_zero]

Goal state after:
Ω : 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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
⊢ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) p μ = 0
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)

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (Arrow.mk (terminal.from G)).augmentedCechNerve ≅ compForgetAugmented G
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : Fin (n + 2) → G
⊢ ((Hom.hom ((standardComplex k G).d (n + 1) n)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x) 1 =
    (d k G (n + 1) ∘ₗ MonoidAlgebra.lsingle x) 1

Tactic:
simp [standardComplex, Action.ofMulAction_V, SimplicialObject.δ, SimplexCategory.δ,
    Fin.succAboveOrderEmb, ← Int.cast_smul_eq_zsmul k ((-1) ^ _ : ℤ), ← ofHom_smul, ← ofHom_sum,
    Representation.IntertwiningMap.coe_toLinearMap, Representation.IntertwiningMap.sum_apply,
    Representation.IntertwiningMap.smul_apply, (Representation.linearizeMap_single),
    smul_eq_mul, mul_one]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (r • x (g.2.1, g.2.2)) - r • x (g.1 * g.2.1, g.2.2) + r • x (g.1, g.2.1 * g.2.2) - r • x (g.1, g.2.1) =
    r • ((A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1))

Tactic:
simp only [map_smul, smul_add, smul_sub]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ iCocycles A 0 ≫ (cochainsIso₀ A).hom = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f

Tactic:
cocyclesIso₀_hom_comp_f

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ iCocycles A 0 ≫ (cochainsIso₀ A).hom = iCocycles A 0 ≫ (cochainsIso₀ A).hom
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 (inhomogeneousCochains.d A 2)) ((ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) = 0

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← inhomogeneousCochains.d_def,
        eq_d₂₃_comp_inv, ModuleCat.hom_comp, LinearMap.comp_apply, cocycles₂.d₂₃_apply x,
        map_zero]

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Coinvariants.ker A.ρ = (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
by
    simp [Representation.FiniteCyclicGroup.coinvariantsKer_eq_range A.ρ g hg, sub_hom,
      Rep.applyAsHom]

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1 = 0

Tactic:
by rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
    (fun f φ => map f φ 1), map₁_one]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
⊢ Function.Injective ⇑(rename ⇑e)

Tactic:
intro _ _ h

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ (optionElim n ?neg✝) none = x none

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ ?m.97 →₀ ℕ

pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ Type ?u.45

Tactic:
h1

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ x none = x none