mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Subsingleton ↥N ∧ Nonempty ↥N
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
have := hN.1

Goal state after:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Subsingleton ↥N ∧ Nonempty ↥N
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
this : Subsingleton ↥N
⊢ ∃ H, N.IsComplement' H
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
this : closure {b | (↑b).IsThreeCycle} = ⊤
⊢ _root_.commutator ↥(alternatingGroup α) = ⊤

Tactic:
rw [eq_top_iff, ← this, Subgroup.closure_le]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
this : closure {b | (↑b).IsThreeCycle} = ⊤
⊢ {b | (↑b).IsThreeCycle} ⊆ ↑(_root_.commutator ↥(alternatingGroup α))
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 4

Tactic:
change _ = 2 ^ 2
  have : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
  apply orderOf_eq_prime_pow
  · intro h
    simp only [pow_one, xa_sq] at h
    injection h with h'
    apply_fun ZMod.val at h'
    apply_fun (· / n) at h'
    simp only [ZMod.val_natCast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self,
      Nat.div_self (NeZero.pos n), reduceCtorEq] at h'
  · simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
      obtain ⟨c, hc⟩ := hk22
      rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
      simp only [commutator, ← hc]
      let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c
      suffices (⊤ : Subgroup (alternatingGroup α)) =
        Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
        rw [this, ← Subgroup.map_commutator]
        refine Subgroup.mem_map_of_mem _ hk
      simp

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case base
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
a✝ : w.head = 1
ih : w.prod • empty = w
⊢ ((base φ) h • w).prod • empty = (base φ) h • w

Tactic:
prod_smul,

Goal state after:
case base
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
a✝ : w.head = 1
ih : w.prod • empty = w
⊢ ((base φ) h * w.prod) • empty = (base φ) h • w
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
hc,

Goal state after:
case pos
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : Nat.Coprime 0 (Nat.card K)
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
hϕ : ∀ (a : K), ϕ a = 1
p : G
k : K
⊢ 0 = ↑0

Tactic:
Int.cast_zero

Goal state after:
G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
hϕ : ∀ (a : K), ϕ a = 1
p : G
k : K
⊢ 0 = 0
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
⊢ ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝¹ : MeasurableSingletonClass β
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝¹ : MeasurableSingletonClass β
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
a : α
⊢ (deterministic id ⋯) a = Measure.dirac a

Tactic:
deterministic_apply,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
a : α
⊢ Measure.dirac (id a) = Measure.dirac a
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (f '' Set.univ) = 1

Tactic:
simp only [Set.image_univ]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (Set.range f) = 1
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' f i)
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' ⋃ i, f i)

Tactic:
have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      · exact h_disj.mono fun _ _ ↦ .preimage _
      · exact fun i ↦ measurable_prodMk_left (hf_meas i)

Goal state after:
case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' f i)
this : ∀ (a : α), (κ a) (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), (κ a) (Prod.mk a ⁻¹' f i)
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' ⋃ i, f i)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel β γ
⊢ η ∘ₖ (μ + κ) = η ∘ₖ μ + η ∘ₖ κ

Tactic:
ext _ _ hs; simp [comp_apply' _ _ _ hs]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (s ×ˢ t).indicator 1 (b, b) ∂κ a = (κ a) (s ∩ t)

Tactic:
Set.indicator_prod_one

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), s.indicator 1 b * t.indicator 1 b ∂κ a = (κ a) (s ∩ t)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), s.indicator 1 b * t.indicator 1 b ∂κ a = ∫⁻ (b : β), (s ∩ t).indicator 1 b ∂κ a

Tactic:
congr with b
    simp [Set.inter_indicator_one]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (η ∘ₖ κ)

Tactic:
refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩
  calc (η ∘ₖ κ) a Set.univ
  _ ≤ κ a Set.univ * η.bound := comp_apply_univ_le κ η a
  _ ≤ κ.bound * η.bound := by gcongr; exact measure_le_bound κ a Set.univ

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
⊢ ((deterministic f hf) x.1).prod ((deterministic g hg) x.2) = (deterministic (Prod.map f g) ⋯) x

Tactic:
deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
⊢ (Measure.dirac (f x.1)).prod (Measure.dirac (g x.2)) = Measure.dirac (Prod.map f g x)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
s : Set α
a✝ : MeasurableSet s
⊢ (μ ⊗ₘ κ).fst s = μ s

Tactic:
rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂κ.snd a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a

Tactic:
snd_eq,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂(κ.map Prod.snd) a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
⊢ (η ∘ₖ κ).snd = η.snd ∘ₖ κ

Tactic:
snd_eq,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
⊢ (η ∘ₖ κ).map Prod.snd = η.map Prod.snd ∘ₖ κ
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : ¬IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

Tactic:
· simp [compProd_of_not_isSFiniteKernel _ _ hη]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0

Tactic:
by
  obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
  simp_rw [compProd_null a mt] at ht
  rw [Filter.eventuallyLE_antisymm_iff]
  exact
    ⟨Filter.EventuallyLE.trans_eq
        (Filter.Eventually.of_forall fun x => measure_mono (Set.preimage_mono hst)) ht,
      Filter.Eventually.of_forall fun x => zero_le⟩

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a✝¹ : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ (((deterministic f hf) a✝¹).prod ((deterministic g hg) a✝¹)) s✝ = ((deterministic (fun a ↦ (f a, g a)) ⋯) a✝¹) s✝

Tactic:
deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a✝¹ : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((Measure.dirac (f a✝¹)).prod (Measure.dirac (g a✝¹))) s✝ = (Measure.dirac (f a✝¹, g a✝¹)) s✝
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᵐ[μ] g
⊢ μ.tilted f = μ.tilted g

Tactic:
have h_int_eq : ∫ x, exp (f x) ∂μ = ∫ x, exp (g x) ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hfg] with x hx
    rw [hx]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᵐ[μ] g
h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ
⊢ μ.tilted f = μ.tilted g
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Tactic:
by
  by_cases hη : IsSFiniteKernel η
  · ext _ _ hs
    simp [compProd_apply hs]
  · simp [hη]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
⊢ rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal → rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
hx_exp_log

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : -llr μ ν x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal

Tactic:
hx_exp_log

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : -llr μ ν x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ (ν.rnDeriv μ x).toReal = (ν.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : (-llr ν μ) x = llr μ ν x
⊢ rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal → rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
hx_exp_log

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : (-llr ν μ) x = llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : llr ν μ x = -llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal

Tactic:
hx_exp_log

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : llr ν μ x = -llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ (ν.rnDeriv μ x).toReal = (ν.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ llr (c⁻¹ • μ) ν =ᵐ[μ] llr μ (c • ν)

Tactic:
have hc' : c⁻¹ ≠ 0 := by simp [hc_ne_top]
  have hc_ne_top' : c⁻¹ ≠ ∞ := by simp [hc]
  filter_upwards [llr_smul_left hμν c⁻¹ hc' hc_ne_top', llr_smul_right hμν c hc hc_ne_top] with
    x hx_left hx_right
  rw [hx_left, hx_right]
  simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
⊢ llr (c • μ) (c • ν) =ᵐ[μ] llr μ ν

Tactic:
by
  simp_rw [← Measure.coe_nnreal_smul]
  filter_upwards [llr_smul_same hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx
  rw [hx]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ Integrable (fun p ↦ f p.2) (μ ⊗ₘ κ) ↔ Integrable f (⇑κ ∘ₘ μ)

Tactic:
rw [← Measure.snd_compProd, Measure.snd, integrable_map_measure _ measurable_snd.aemeasurable,
    Function.comp_def]
  rwa [← Measure.snd, Measure.snd_compProd]

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case pos
x : ℝ
h0 : x = 0
⊢ deriv klFun 0 = 0

Tactic:
exact deriv_zero_of_not_differentiableAt not_differentiableAt_klFun_zero

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ klDiv μ μ = 0

Tactic:
have h := llr_self μ
  rw [klDiv_def, if_pos]
  · simp [integral_congr_ae h]
  · rw [integrable_congr h]
    exact ⟨Measure.AbsolutelyContinuous.rfl, integrable_zero _ _ μ⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfν : Integrable (fun x ↦ rexp (f x)) ν
⊢ Integrable (llr μ (ν.tilted f)) μ

Tactic:
by
  rw [integrable_congr (llr_tilted_right hμν hfν)]
  exact Integrable.add (hfμ.neg.add (integrable_const _)) h_int

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ a ∈ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
suffices h_meas_eq : μ { x | ¬f x ≤ a } = μ.trim hm { x | ¬f x ≤ a } by
    simp_rw [Set.mem_ofPred_eq, ae_iff, h_meas_eq]

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ μ {x | ¬f x ≤ a} = (μ.trim hm) {x | ¬f x ≤ a}
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ 0 ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Tactic:
· positivity

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : ¬m ≤ m₀
⊢ Integrable μ[f | m] μ

Tactic:
rw [condExp_of_not_le hm]; exact integrable_zero _ _ _

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsMarkovKernel κ
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ ¬μ ≪ ν

Tactic:
rwa [Measure.absolutelyContinuous_compProd_left_iff] at h_ac

Goal state after: