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

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
⊢ (Nat.card ↥(comap K.subtype N)).Coprime N.index

Tactic:
exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
i : ↥g.cycleFactorsFinset
⊢ ⟨↑i, ⋯⟩ ∈ ↑(toPermHom g).ker

Tactic:
exact Perm.ext fun x ↦ Subtype.ext (cycleFactorsFinset_mem_commute' g i.2 x.2).mul_inv_cancel

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range ≤ centralizer {g}

Tactic:
rw [kerParam_range_eq]
  exact map_subtype_le (toPermHom g).ker

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ ∀ (a b c : QuaternionGroup n), a * b * c = a * (b * c)

Tactic:
rintro (i | i) (j | j) (k | k) <;> simp only [mul]

Goal state after:
case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (i + j + k) = a (i + (j + k))

case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (i + j)) = xa (k - j - i)

case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (j - i + k) = xa (j + k - i)

case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (j - i)) = a (i + (↑n + k - j))

case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (i + j + k) = xa (i + (j + k))

case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (i + j)) = a (↑n + (k - j) - i)

case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + j - i + k) = a (↑n + (j + k) - i)

case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (↑n + j - i)) = xa (i + (↑n + k - j))
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ Subgroup.map (ofSubtype ↑⟨(↑g).support, ⋯⟩) (kleinFour ↥↑⟨(↑g).support, ⋯⟩)

Tactic:
mem_map_kleinFour_ofSubtype

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ (↑g).support ⊆ ↑⟨(↑g).support, ⋯⟩ ∧ (↑g = 1 ∨ (↑g).cycleType = {2, 2})

case hs
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ (↑⟨(↑g).support, ⋯⟩).card = 4
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ Monoid.exponent G = Nat.card G

Tactic:
refine dvd_antisymm Group.exponent_dvd_nat_card ?_

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ Nat.card G ∣ Monoid.exponent 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
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
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h : ϕ k = ↑n + ↑1
⊢ k • g * g⁻¹ = g ^ n

Tactic:
← Int.cast_add

Goal state after:
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
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h : ϕ k = ↑(n + 1)
⊢ k • g * g⁻¹ = g ^ n
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
⊢ κ y' = κ y

Tactic:
ext s hs
  exact mem_of_mem_measurableAtom hy' (κ.measurable_coe hs (measurableSet_singleton (κ y s))) rfl

Goal state after:
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:
by
  rw [deterministic_apply, lintegral_dirac (g a) f]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel Kernel.id

Tactic:
rw [Kernel.id]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic id ⋯)
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y < 1 ↔ x = y

Tactic:
rw [Nat.lt_one_iff, hammingDist_eq_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (copy α)

Tactic:
rw [copy]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
⊢ ∫⁻ (x : β), f x ∂(const α μ) a = ∫⁻ (x : β), f x ∂μ

Tactic:
by rw [const_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
s : Set β
⊢ ∫⁻ (x : β) in s, f x ∂(const α μ) a = ∫⁻ (x : β) in s, f x ∂μ

Tactic:
by rw [const_apply]

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
x : List α
hx : x ∈ {x ∈ T | x.length = s}
⊢ (1 / ↑(Fintype.card α)) ^ x.length = (1 / ↑(Fintype.card α)) ^ s

Tactic:
simp [Finset.mem_filter.mp hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
⊢ ((piecewise hs κ η) a) t = if a ∈ s then (κ a) t else (η a) t

Tactic:
rw [piecewise_apply]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
⊢ (if a ∈ s then κ a else η a) t = if a ∈ s then (κ a) t else (η a) t
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
⊢ Measurable fun b ↦ (η (a, b)) {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}

Tactic:
refine (measurable_kernel_prodMk_left ?_).comp measurable_prodMk_left

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
⊢ MeasurableSet {p | (p.1.2, p.2) ∈ s}
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 γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∫⁻ (b : β), ∑' (i : ι), ((η i) b) s✝ ∂κ a✝ = ∑' (i : ι), ∫⁻ (b : β), ((η i) b) s✝ ∂κ a✝

Tactic:
rw [lintegral_tsum]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∀ (i : ι), AEMeasurable (fun b ↦ ((η i) b) s✝) (κ a✝)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel κ.swapRight

Tactic:
rw [Kernel.swapRight_eq]; exact IsMarkovKernel.map _ measurable_swap

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0
a : α
ha_zero : (η a) (Prod.mk a ⁻¹' s) = 0 a
⊢ κ a ≪ η a → (κ a) (Prod.mk a ⁻¹' s) = 0 a

Tactic:
ha_ac

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0
a : α
ha_zero : (η a) (Prod.mk a ⁻¹' s) = 0 a
ha_ac : κ a ≪ η a
⊢ (κ a) (Prod.mk a ⁻¹' s) = 0 a
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 β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
this : ∀ (b : β), (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b
⊢ ∫⁻ (b : β), s.indicator (fun x ↦ 1) b ∂κ x = (κ x) s

Tactic:
rw [lintegral_indicator_const hs, one_mul]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ

Tactic:
by
    calc ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ)
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) := by
      simp_rw [← comp_assoc, swap_swap, id_comp]
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ)) := by rw [this]
    _ = ξ ∘ₖ η ∥ₖ κ := by simp_rw [← comp_assoc, swap_swap, id_comp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) s) =ᵐ[μ] 0
a : α
ha_zero : (η a) s = 0 a
⊢ κ a ≪ η a → (κ a) s = 0 a

Tactic:
ha_ac

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) s) =ᵐ[μ] 0
a : α
ha_zero : (η a) s = 0 a
ha_ac : κ a ≪ η a
⊢ (κ a) s = 0 a
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case pos.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
⊢ Tendsto f' atTop (𝓝 fun x ↦ ∫ (y : β), f y ∂κ x)

Tactic:
rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_ofPred_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · simp [f', hfx, integral_undef]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f y ∂κ x

Tactic:
by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
  let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
  refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
  · refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    simp_rw [SimpleFunc.integral_eq]
    refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    exact κ.measurable_coe ((s n).measurableSet_fiber _)
  · rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_ofPred_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · simp [f', hfx, integral_undef]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
⊢ μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'

Tactic:
rwa [Measure.ae_ennreal_smul_measure_eq] at h1'

Goal state after:
case hc
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
⊢ (ν univ)⁻¹ ≠ 0
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
h_smul : ∀ (c : ℝ≥0) (a : ℝ), c • a = ↑c * a
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    ↑c * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)

Tactic:
simp only [measureReal_nnreal_smul_apply, integral_smul_nnreal_measure, h_smul, NNReal.coe_inv]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
h_smul : ∀ (c : ℝ≥0) (a : ℝ), c • a = ↑c * a
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + ↑c * ν.real univ - μ.real univ =
    ↑c * ((↑c)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c)⁻¹ * μ.real univ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
⊢ ↑↑↑f =ᵐ[μ] 0

Tactic:
by
  obtain ⟨g, hg_sm, hfg⟩ := lpMeas.ae_fin_strongly_measurable' hm f hp_ne_zero hp_ne_top
  refine hfg.trans ?_
  refine ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim hm ?_ ?_ hg_sm
  · intro s hs hμs
    have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
    rw [IntegrableOn, integrable_congr hfg_restrict.symm]
    exact hf_int_finite s hs hμs
  · intro s hs hμs
    have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
    rw [integral_congr_ae hfg_restrict.symm]
    exact hf_zero s hs hμs

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
h_int_right : Integrable (llr μ (c • ν)) μ
⊢ klDiv (c⁻¹ • μ) ν ≠ ∞

Tactic:
exact klDiv_ne_top (hμν.smul_left _) h_int_left

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun x ↦ c
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
⊢ μ.real Set.univ ≠ 0

Tactic:
Ne,

Goal state after:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun x ↦ c
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
⊢ ¬μ.real Set.univ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]

Tactic:
by_cases hm : m ≤ m₀
  swap; · simp_rw [condExp_of_not_le hm]; simp
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; simp
  refine (condExp_ae_eq_condExpL1 hm _).trans ?_
  rw [condExpL1_smul c f]
  refine (condExp_ae_eq_condExpL1 hm f).mp ?_
  refine (coeFn_smul c (condExpL1 hm μ f)).mono fun x hx1 hx2 => ?_
  simp only [hx1, hx2, Pi.smul_apply]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
⊢ (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[fun y ↦ T (f y) + a | m]

Tactic:
by
  have hp : (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[T ∘ f | m] + μ[(fun y ↦ a) | m] := by
    filter_upwards [T.comp_condExp_comm hf_int] with b hb
    simpa [condExp_const hm a]
  exact hp.trans (condExp_add (T.integrable_comp hf_int) (integrable_const a) m).symm

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

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)

Tactic:
exact integrable_condExp.indicator (hm _ ht)

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
rw [setLIntegral_trim hm (measurable_condLExp _ _ _) hs, setLIntegral_condLExp _ _ _ hs]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
by
  rw [setLIntegral_trim hm (measurable_condLExp _ _ _) hs, setLIntegral_condLExp _ _ _ hs]

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
⊢ μ⁻[fun x ↦ ‖f x‖ₑ | m] =ᵐ[μ] fun x ↦ ‖μ[f | m] x‖ₑ

Tactic:
by
  have A : μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] =ᵐ[μ] μ⁻[fun x ↦ ‖f x‖ₑ | m] := by
    apply condLExp_congr_ae
    filter_upwards [h'f] with x hx using by simp [Real.enorm_eq_ofReal hx]
  grw [← A, condLExp_ofReal m hf h'f]
  filter_upwards [condExp_nonneg h'f (m := m)] with x hx using by simp [Real.enorm_eq_ofReal hx]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
V : Type u_2
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : Module A V
inst✝ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
⊢ Function.Bijective (⇑(Finsupp.linearCombination R ⇑b) ∘ ⇑j)

Tactic:
j.bijective.of_comp_iff

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
V : Type u_2
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : Module A V
inst✝ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
⊢ Function.Bijective ⇑(Finsupp.linearCombination R ⇑b)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁷ : CommSemiring R
V : Type u_2
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module R V
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Module A V
inst✝¹ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst✝ : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
⊢ Function.Bijective (⇑(Fintype.linearCombination R ⇑b) ∘ ⇑j)

Tactic:
j.bijective.of_comp_iff

Goal state after:
case refine_1
R : Type u_1
inst✝⁷ : CommSemiring R
V : Type u_2
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module R V
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Module A V
inst✝¹ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst✝ : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
⊢ Function.Bijective ⇑(Fintype.linearCombination R ⇑b)