mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ({1} ∪ {g | (↑g).cycleType = {2, 2}}).card ≤ 4

Tactic:
apply (Finset.card_union_le _ _).trans

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ {1}.card + {g | (↑g).cycleType = {2, 2}}.card ≤ 4
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ (kleinFour α).Characteristic

Tactic:
by
  obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  have _ := subsingleton_two_sylow hα4
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
  exact Sylow.characteristic_of_subsingleton _

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : 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)
i : ι
g : G i
w : NormalWord d
⊢ (equivPair i).symm
      (let __src := (equivPair i) w;
      { head := g * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ }) =
    g • w

Tactic:
summand_smul_def'

Goal state after:
ι : 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)
i : ι
g : G i
w : NormalWord d
⊢ (equivPair i).symm
      (let __src := (equivPair i) w;
      { head := g * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ }) =
    (equivPair i).symm
      (let __src := (equivPair i) w;
      { head := g * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ })
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ Subgroup.centralizer {g} ≤ alternatingGroup α ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

Tactic:
by
  rw [SetLike.le_def]
  constructor
  · intro h
    exact ⟨odd_of_centralizer_le_alternatingGroup h,
      card_le_of_centralizer_le_alternating h,
      count_le_one_of_centralizer_le_alternating h⟩
  · rintro ⟨h_odd, h_fixed, h_count⟩ x hx
    rw [← kerParam_range_eq_centralizer_of_count_le_one h_count] at hx
    obtain ⟨⟨y, uv⟩, rfl⟩ := MonoidHom.mem_range.mp hx
    rw [mem_alternatingGroup, sign_kerParam_apply_apply (g := g) y uv]
    convert! mul_one _
    · apply Finset.prod_eq_one
      rintro ⟨c, hc⟩ _
      obtain ⟨k, hk⟩ := (uv _).prop
      rw [← hk, map_zpow]
      convert! one_zpow k
      rw [IsCycle.sign, Odd.neg_one_pow, neg_neg]
      · apply h_odd
        rw [cycleType_def, Multiset.mem_map]
        exact ⟨c, hc, rfl⟩
      · rw [mem_cycleFactorsFinset_iff] at hc
        exact hc.left
    · suffices y = 1 by simp [this]
      have := card_fixedPoints g
      exact card_support_le_one.mp <| le_trans (Finset.card_le_univ _) (by lia)

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

Goal state before:
pp: α : 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 α
⊢ ¬Subgroup.center ↥(alternatingGroup α) = ⊤

Tactic:
center_eq_bot (le_of_eq hα4.symm)

Goal state after:
α : 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 α
⊢ ¬⊥ = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ orderOf (xa m) ∣ lcm (2 * n) 4

Tactic:
orderOf_xa

Goal state after:
case inr.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 4 ∣ lcm (2 * n) 4
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum (κs n).seq) a) s = ((Kernel.sum fun n ↦ (κs (e n).1).seq (e n).2) a) s

Tactic:
simp_rw [Kernel.sum_apply' _ _ hs]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι) (n_1 : ℕ), (((κs n).seq n_1) a) s = ∑' (n : ℕ), (((κs (e n).1).seq (e n).2) a) s
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
⊢ (κ.restrict ⋯) a = κ a

Tactic:
rw [Kernel.restrict_apply, Measure.restrict_univ]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) → ∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s

pp: case mpr
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ (∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s) →
    s ∈ uniformity (Hamming β)

Tactic:
· refine fun hs ↦ ⟨1, zero_lt_one, fun hab ↦ hs <| by simpa using hab⟩

Goal state after:
case mpr
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ (∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s) →
    s ∈ uniformity (Hamming β)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comapRight ⋯ = κ

Tactic:
by
  ext _ _ hs; rw [comapRight_apply' _ _ _ hs]; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ Kernel.id ∘ₖ κ = κ

Tactic:
by
  ext a s hs
  simpa [comp_apply' _ _ _ hs, id_apply, Measure.dirac_apply' _ hs]
    using lintegral_indicator_one hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)

Tactic:
rw [← Kernel.kernel_sum_seq κ]
  have (a : _) : Kernel.sum (Kernel.seq κ) a (Prod.mk a ⁻¹' t) =
      ∑' n, Kernel.seq κ n a (Prod.mk a ⁻¹' t) :=
    Kernel.sum_apply' _ _ (measurable_prodMk_left ht)
  simp_rw [this]
  refine Measurable.tsum fun n => ?_
  exact measurable_kernel_prodMk_left_of_finite ht inferInstance

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

Goal state before:
pp: case calc.step
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := ⋯
T : Finset (List α) := ⋯
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc r (r * maxLen)
D : ℝ := ⋯
⊢ ∑ i ∈ Finset.Icc r (r * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑r * ↑maxLen

Tactic:
rcases r with (_ | _ | r) <;> rcases maxLen with (_ | _ | maxLen)
    <;> simp at * <;> norm_cast

Goal state after:
case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
hr : True
hlen_maps : ∀ x ∈ T, x.length = r + 1 + 1
⊢ 0 ≤ r + 1

case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hr : True
hlen_maps : ∀ x ∈ T, r + 1 < x.length ∧ x.length ≤ (r + 1 + 1) * (maxLen + 1 + 1)
⊢ (r + 1 + 1) * (maxLen + 1 + 1) - (r + 1) ≤ (r + 1 + 1) * (maxLen + 1 + 1)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ ∀ ⦃f g : SimpleFunc (α × β) ℝ≥0∞⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (Measurable fun a ↦ ∫⁻ (b : β), f (a, b) ∂κ a) →
        (Measurable fun a ↦ ∫⁻ (b : β), g (a, b) ∂κ a) → Measurable fun a ↦ ∫⁻ (b : β), (f + g) (a, b) ∂κ a

Tactic:
intro g₁ g₂ _ hm₁ hm₂

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ⇑g₁) (support ⇑g₂)
hm₁ : Measurable fun a ↦ ∫⁻ (b : β), g₁ (a, b) ∂κ a
hm₂ : Measurable fun a ↦ ∫⁻ (b : β), g₂ (a, b) ∂κ a
⊢ Measurable fun a ↦ ∫⁻ (b : β), (g₁ + g₂) (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

Tactic:
simp only [map, hf, ↓reduceDIte]
    rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

Tactic:
simp only [map, hf, ↓reduceDIte]
    rfl

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 γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ (κ ×ₖ η).fst = κ

Tactic:
rw [prod, fst_comp]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ (κ ∥ₖ η).fst ∘ₖ copy α = κ
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✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable (f x) (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
⊢ StronglyMeasurable fun x ↦ ∑ x_1 ∈ (s n).range, (κ x).real (⇑(s' n x) ⁻¹' {x_1}) • x_1

Tactic:
refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable (f x) (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ StronglyMeasurable fun x_1 ↦ (κ x_1).real (⇑(s' n x_1) ⁻¹' {x}) • x
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
p✝ q✝ r✝ : Prop
h : r✝ → p✝
⊢ (r✝ ↔ p✝ ∧ q✝) ↔ p✝ → (r✝ ↔ q✝)

Tactic:
by
    rw [← and_congr_right_iff, and_iff_right_of_imp h]

Goal state after:
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ (((κ ⊗ₖ η).comapRight ⋯) a) t = ((κ ⊗ₖ η.comapRight hf) a) t

Tactic:
comapRight_apply' _ _ _ ht,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ ((κ ⊗ₖ η) a) (Prod.map id f '' t) = ((κ ⊗ₖ η.comapRight hf) a) t
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ (μ.tilted f).tilted (-f) = (μ Set.univ)⁻¹ • μ

Tactic:
rw [tilted_tilted hf]; simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
⊢ (μ.tilted f).rnDeriv μ =ᵐ[μ] fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)

Tactic:
refine (rnDeriv_tilted_left μ hf).trans ?_
  filter_upwards [Measure.rnDeriv_self μ] with x hx
  rw [hx, mul_one]

Goal state after:
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 ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s ≤
    ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s

Tactic:
have h_meas_nonpos_g : MeasurableSet[m] {x | g x ≤ 0} :=
    hg.measurableSet_le (@stronglyMeasurable_const _ _ m _ _)

Goal state after:
α : 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 ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s ≤
    ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : Fact (m ≤ m0)
inst✝ : CompleteSpace F
hp : Fact (1 ≤ p)
⊢ CompleteSpace ↥(lpMeas F 𝕜 m p μ)

Tactic:
by
  rw [(lpMeasSubgroupToLpMeasIso F 𝕜 p μ).symm.completeSpace_iff]; infer_instance

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

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
⊢ ∀ (f : ↥(Lp F p μ)), AEStronglyMeasurable (↑↑f) μ → P f

Tactic:
by
  intro f hf
  let f' := (⟨f, hf⟩ : lpMeas F ℝ m p μ)
  let g := lpMeasToLpTrimLie F ℝ p μ hm f'
  have hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g := by
    simp only [f', g, LinearIsometryEquiv.symm_apply_apply]
  change P ↑f'
  rw [hfg]
  refine
    @Lp.induction α F m _ p (μ.trim hm) _ hp_ne_top
      (fun g => P ((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) ?_ ?_ ?_ g
  · intro b t ht hμt
    rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator ht hμt.ne b]
    have hμt' : μ t < ∞ := (le_trim hm).trans_lt hμt
    specialize h_ind b ht hμt'
    rwa [Lp.simpleFunc.coe_indicatorConst] at h_ind
  · intro f g hf hg h_disj hfP hgP
    rw [LinearIsometryEquiv.map_add]
    push_cast
    have h_eq :
      ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
        ((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf) : Lp F p μ) =
          (memLp_of_memLp_trim hm hf).toLp f :=
      lpMeasToLpTrimLie_symm_toLp hm
    rw [h_eq f hf] at hfP ⊢
    rw [h_eq g hg] at hgP ⊢
    exact h_add (memLp_of_memLp_trim hm hf) (memLp_of_memLp_trim hm hg)
      (hf.aestronglyMeasurable.of_trim hm) (hg.aestronglyMeasurable.of_trim hm) h_disj hfP hgP
  · change IsClosed ((lpMeasToLpTrimLie F ℝ p μ hm).symm ⁻¹' {g : lpMeas F ℝ m p μ | P ↑g})
    exact IsClosed.preimage (LinearIsometryEquiv.continuous _) h_closed

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

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ENNReal.ofReal (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + (ν univ).toReal - (μ univ).toReal) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal +
        (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ + (μ univ).toReal - (μ univ).toReal))

Tactic:
add_sub_cancel_right

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ENNReal.ofReal (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + (ν univ).toReal - (μ univ).toReal) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal + ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᵐ[μ]
    s.indicator μ[s.indicator f | m]

Tactic:
rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]

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

Goal state before:
pp: case refine_3.refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ Continuous fun f ↦ ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm f)

Tactic:
refine continuous_induced_dom.comp ?_
      exact LinearIsometryEquiv.continuous _

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

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable P⁻[X | mΩ]

Tactic:
by_cases hX : Measurable[mΩ] X

Goal state after:
case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
hX : Measurable X
⊢ Measurable P⁻[X | mΩ]

case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
hX : ¬Measurable X
⊢ Measurable P⁻[X | mΩ]
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 = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
by_cases hX : Measurable[mΩ] X

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

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