mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case h₁
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
θ : Θ
⊢ ∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y ≤ ℓ θ y

Tactic:
lintegral_dirac' _ (by fun_prop)

Goal state after:
case h₁
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
θ : Θ
⊢ ℓ θ y ≤ ℓ θ y
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t, ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂⇑κ ∘ₘ μ = (μ ⊗ₘ κ) (s ×ˢ t)

Tactic:
← swap_compProd_posterior,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t, ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂⇑κ ∘ₘ μ =
    (⇑(Kernel.swap 𝓧 Ω) ∘ₘ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ) (s ×ˢ t)
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:

Tactic:
π ⊗ₘ (κ ∘ₖ P) = (Kernel.id ∥ₖ κ) ∘ₘ (π ⊗ₘ P) := Measure.parallelComp_comp_compProd.symm
  _ = (Kernel.id ∥ₖ κ) ∘ₘ ((P†π) ×ₖ Kernel.id) ∘ₘ P ∘ₘ π := by rw [posterior_prod_id_comp]
  _ = ((P†π) ×ₖ κ) ∘ₘ P ∘ₘ π := by
      rw [Measure.comp_assoc, Kernel.parallelComp_comp_prod, Kernel.id_comp, Kernel.comp_id]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))

Tactic:
convert! mf

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀) = (traj κ a) x₀
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hfm
X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ AEStronglyMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))

Tactic:
convert! mf

Goal state after:
X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀) = (traj κ a) x₀
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : ↑I
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ ∀ᵐ (ω : Ω) ∂P, X ω ≤ n

Tactic:
by
  rw [hX.ae_iff (p := (· ≤ n)) <| by fun_prop, binomial,
    ae_map_iff (by fun_prop) (finite_Iic _).measurableSet]
  filter_upwards [setBernoulli_ae_subset] with s hs
  simpa using ncard_le_ncard hs

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

Goal state before:
pp: case h₁
n : ℕ
p : ↑I
k : ℕ
⊢ k ∉ Finset.Iic n → (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k} = 0

Tactic:
simp_all [Nat.choose_eq_zero_of_lt]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ ⇑(condExpKernel μ m) ∘ₘ μ.trim hm = μ

Tactic:
rw [← Measure.snd_compProd, compProd_trim_condExpKernel]

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ (Measure.map Function.diag μ).snd = μ
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : s ∈ {A}
t : Set 𝓧
ht : MeasurableSet t
⊢ P (A ∩ X ⁻¹' t) = P A * P (X ⁻¹' t)

Tactic:
have hA' : A = A.indicator (1 : Ω → ℝ) ⁻¹' {1} := by ext; simp [Set.indicator]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : s ∈ {A}
t : Set 𝓧
ht : MeasurableSet t
hA' : A = A.indicator 1 ⁻¹' {1}
⊢ P (A ∩ X ⁻¹' t) = P A * P (X ⁻¹' t)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_self h_le h_indep hf hns hnsp hns_univ).indepSet_of_measurableSet ht_tail
      ht_tail)
  filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

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

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
⊢ (ε ≫ Δ).hom = (Δ ≫ (ε ⊗ₘ ε)).hom

Tactic:
simp only [WideSubcategory.comp_def, MorphismProperty.counit_hom]

Goal state after:
X Y : Stoch
κ : X ⟶ Y
⊢ ε ≫ Δ.hom = Δ.hom ≫ (ε ⊗ₘ ε).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X Y Z : SFinKer
⊢ { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ } ≫
      { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ } =
    𝟙
      { carrier := { carrier := X.carrier × Y.carrier, str := Prod.instMeasurableSpace }.carrier × Z.carrier,
        str := Prod.instMeasurableSpace }

pp: case refine_2
X Y Z : SFinKer
⊢ { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ } ≫
      { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ } =
    𝟙
      { carrier := X.carrier × { carrier := Y.carrier × Z.carrier, str := Prod.instMeasurableSpace }.carrier,
        str := Prod.instMeasurableSpace }

Tactic:
· ext : 1; dsimp
      rw [Kernel.deterministic_comp_deterministic, Kernel.id]
      rfl

Goal state after:
case refine_2
X Y Z : SFinKer
⊢ { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ } ≫
      { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ } =
    𝟙
      { carrier := X.carrier × { carrier := Y.carrier × Z.carrier, str := Prod.instMeasurableSpace }.carrier,
        str := Prod.instMeasurableSpace }
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X Y Z : SFinKer
⊢ { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ } ≫
      { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ } =
    𝟙
      { carrier := X.carrier × { carrier := Y.carrier × Z.carrier, str := Prod.instMeasurableSpace }.carrier,
        str := Prod.instMeasurableSpace }

Tactic:
· ext : 1; dsimp
      rw [Kernel.deterministic_comp_deterministic, Kernel.id]
      rfl

Goal state after:
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✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ stoppedValue f τ =ᵐ[μ] μ[f n | hτ.measurableSpace]

Tactic:
have : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i} := by
    ext1 x
    simp only [Set.mem_univ, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_iUnion, Set.mem_ofPred_eq, exists_apply_eq_apply']

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✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
⊢ stoppedValue f τ =ᵐ[μ] μ[f n | hτ.measurableSpace]
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • (X ω - deriv (cgf X μ) t) ^ 2 ∂μ =
    (∫ (x : Ω), (fun ω ↦ (X ω - deriv (cgf X μ) t) ^ 2 * rexp (t * X ω)) x ∂μ) / mgf X μ t

Tactic:
← integral_div

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • (X ω - deriv (cgf X μ) t) ^ 2 ∂μ =
    ∫ (a : Ω), (X a - deriv (cgf X μ) t) ^ 2 * rexp (t * X a) / mgf X μ t ∂μ
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case add
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 ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ (x + y) • v ∈ σ.toSubmodule.carrier

Tactic:
add_smul

Goal state after:
case add
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 ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ x • v + y • v ∈ σ.toSubmodule.carrier
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case add
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
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ (x + y) • m ∈ σ.toSubmodule.carrier

Tactic:
add_smul

Goal state after:
case add
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
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ x • m + y • 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✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess
      (fun i ↦
        ({a | ⊥ < hqX.localSeq n a} ∩ {a | ⊥ < hpX.localSeq n a}).indicator (stoppedProcess X (hpX.localSeq n) i))
      (hqX.localSeq n) i ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω

Tactic:
← Set.indicator_indicator

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

Goal state before:
pp: Ω : 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 ρ
j : ℕ
hj : j ∈ range K
⊢ ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ = ∑ i ∈ Ico j N, ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals_Ico ((mem_range.1 hj).le.trans hKN)]

Goal state after:
Ω : 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 ρ
j : ℕ
hj : j ∈ range K
⊢ ∀ k ∈ Set.Ico j N, IntervalIntegrable (fun x ↦ 1) ρ ↑k ↑(k + 1)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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 ρ
⊢ (∫ (a : Ω), X a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1

Tactic:
gcongr
        rw [intervalIntegral.integral_of_le (Nat.cast_nonneg _)]
        simp only [integral_const, measureReal_restrict_apply', measurableSet_Ioc, Set.univ_inter,
          smul_eq_mul, mul_one]
        rw [← ENNReal.toReal_one]
        exact ENNReal.toReal_mono ENNReal.one_ne_top prob_le_one

Goal state after:
Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
⊢ Module.finrank k V = 1

Tactic:
have : Nontrivial V := IsSimpleModule.nontrivial A V

Goal state after:
A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
⊢ Module.finrank k V = 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 α
f : α →₀ V
w : W
⊢ (σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w) = f.sum fun i v ↦ single i (v ⊗ₜ[k] w)

Tactic:
by
  simp [finsuppTensorLeft, TensorProduct.finsuppLeft_apply_tmul]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: 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

Tactic:
· simp only [coindFunctor_obj, coindFunctor_map, hom_ofHom,
        Representation.coindMap_coe_apply_apply, hom_comm_apply, x]
      simp_all [← y.2 (γ g), γ]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
⊢ Coinvariants.ker (leftRegular k G) = ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

Tactic:
refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_

Goal state after:
case refine_1
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
⊢ (Set.range fun gv ↦ ((leftRegular k G) gv.1) gv.2 - gv.2) ⊆
    ↑((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

case refine_2
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
⊢ x ∈ Coinvariants.ker (leftRegular k G)
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case neg
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
g : G
hg : ¬g = 1
⊢ x.coeff g = (x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r).coeff g

Tactic:
· simp_all [sum_apply', MonoidAlgebra.coeff_finsuppSum]

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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h, ↑(f h) * h z = g (∑ h, ↑(f h) * h z) * ↑(f g)

Tactic:
map_sum,

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h, ↑(f h) * h z = (∑ x, g (↑(f x) * x z)) * ↑(f g)
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ QuasiIso (εToSingle₀ k G)

Tactic:
rw [← HomologicalComplex.quasiIso_map_iff_of_preservesHomology _ (forget₂ _ (ModuleCat.{u} k))]
  apply quasiIso_forget₂_εToSingle₀

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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n ≫
      map (↑e.symm) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n =
    𝟙 (groupCohomology A n)

Tactic:
by
    rw [← groupCohomology.map_comp, ← groupCohomology.map_id]
    exact groupCohomology.map_congr (by simp) e'.comp_symm n

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

Goal state before:
pp: case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g h : G
⊢ (QuotientGroup.leftRel S) g h → ⟨↑x g - (A.ρ g) y + y, ⋯⟩ = ⟨↑x h - (A.ρ h) y + y, ⋯⟩

Tactic:
hgh

Goal state after:
case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g h : G
hgh : (QuotientGroup.leftRel S) g h
⊢ ⟨↑x g - (A.ρ g) y + y, ⋯⟩ = ⟨↑x h - (A.ρ h) y + y, ⋯⟩
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_3.H.H
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g h : G
⊢ Quotient.liftOn' (↑g * ↑h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
    ((A.quotientToInvariants S).ρ ↑g) (Quotient.liftOn' (↑h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
      Quotient.liftOn' (↑g) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯

Tactic:
| @H h =>

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
have nat := η.hom.hom.naturality mulRepHom

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app (rightFDRep ⊗ rightFDRep) ≫ (forget k G).map mulRepHom
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g