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

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ π * swap a b * σ * ↑⟨π * swap a b, ⋯⟩⁻¹ = π * σ * π⁻¹

Tactic:
have hd : Disjoint (swap a b) σ := by
        rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left,
          Finset.disjoint_singleton_left]
        exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩

Goal state after:
case inr.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
hd : (swap a b).Disjoint σ
⊢ π * swap a b * σ * ↑⟨π * swap a b, ⋯⟩⁻¹ = π * σ * π⁻¹
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x✝ : IsCyclic ↥(alternatingGroup α)
⊢ Nat.card α ≤ 3

Tactic:
rw [← isMulCommutative_iff_card_le_three]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x✝ : IsCyclic ↥(alternatingGroup α)
⊢ IsMulCommutative ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g : Perm α
⊢ g ∈ G ↔ g ∈ alternatingGroup α

Tactic:
refine swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ swap x y * g ∈ G ↔ swap x y * g ∈ alternatingGroup α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty (Fin s.ncard ≃ ↑s)
y : Fin s.ncard ↪ ↑s := (Classical.choice this).toEmbedding
⊢ ∀ ⦃a : α⦄,
    a ∈ Set.range ⇑(y.trans (subtype fun x ↦ x ∈ s)) →
      ∀ ⦃b : α⦄, b ∈ Set.range ⇑(x.trans (subtype fun x ↦ x ∈ ofFixingSubgroup M s)) → a ≠ b

Tactic:
rintro _ ⟨j, rfl⟩ _ ⟨i, rfl⟩ H

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty (Fin s.ncard ≃ ↑s)
y : Fin s.ncard ↪ ↑s := (Classical.choice this).toEmbedding
j : Fin s.ncard
i : Fin n
H : (y.trans (subtype fun x ↦ x ∈ s)) j = (x.trans (subtype fun x ↦ x ∈ ofFixingSubgroup M s)) i
⊢ False
Module: Mathlib.GroupTheory.GroupAction.OfQuotient

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : MulAction G A
H : Subgroup G
inst✝ : H.Normal
g : G ⧸ H
a : ↑(fixedPoints (↥H) A)
| g • a

Tactic:
← g.out_eq

Goal state after:
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : MulAction G A
H : Subgroup G
inst✝ : H.Normal
g : G ⧸ H
a : ↑(fixedPoints (↥H) A)
| ⟦Quotient.out g⟧ • a
Module: Mathlib.GroupTheory.GroupAction.OfQuotient

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : MulAction G A
H : Subgroup G
inst✝ : H.Normal
g : G ⧸ H
a : ↑(fixedPoints (↥H) A)
⊢ Quotient.out g • a = g • a

Tactic:
conv_rhs => rw [← g.out_eq]

Goal state after:
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : MulAction G A
H : Subgroup G
inst✝ : H.Normal
g : G ⧸ H
a : ↑(fixedPoints (↥H) A)
⊢ Quotient.out g • a = ⟦Quotient.out g⟧ • a
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e ∈ S.rightHom.ker

Tactic:
MonoidHom.mem_ker,

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ S.rightHom ((Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e) = 1
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ (f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e' ∈ S'.rightHom.ker

Tactic:
MonoidHom.mem_ker,

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ S'.rightHom ((f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e') = 1
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
e : E
⊢ e * (s (S.rightHom e))⁻¹ ∈ S.rightHom.ker

Tactic:
MonoidHom.mem_ker,

Goal state after:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
e : E
⊢ S.rightHom (e * (s (S.rightHom e))⁻¹) = 1
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : IsPerfect G
⊢ ¬IsSolvable G

Tactic:
intro h
  exact (h.commutator_lt_top_of_nontrivial G).ne commutator_eq_top

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ∀ (u_1 : ℤˣ) (g : G), (u_1, g) ∈ (u, w.head) :: w.toList → g ∈ d.set u_1

Tactic:
intro u' g' h'
      simp only [List.mem_cons, Prod.mk.injEq] at h'
      rcases h' with ⟨rfl, rfl⟩ | h'
      · exact h1
      · exact w.mem_set _ _ h'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ a.ofPermHom τ ∈ centralizer {g}

Tactic:
by
  rw [mem_centralizer_singleton_iff]
  ext x
  simp only [mul_apply]
  exact ofPermHomFun_commute_zpow_apply a τ x 1

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

Goal state before:
pp: case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support

Tactic:
ofPermHomFun_apply_mem_support_cycle_iff

Goal state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ x ∈ (↑c).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ a.ofPermHomFun τ x ∉ (↑(↑τ c)).support

Tactic:
ofPermHomFun_apply_mem_support_cycle_iff

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ x ∉ (↑c).support
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : (-1) ^ #c.support ≠ 1
⊢ Odd ((card ∘ support) c)

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : sign c = 1
⊢ c.IsCycle

Tactic:
· rw [← Nat.not_even_iff_odd, comp_apply]
      exact fun h ↦ this h.neg_one_pow

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : sign c = 1
⊢ c.IsCycle
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 φ
⊢ empty.prod = 1

Tactic:
simp [prod, empty]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ ∃ x_1 ∈ (toPermHom g).ker, (Subgroup.centralizer {g}).subtype x_1 = x

Tactic:
MonoidHom.mem_ker,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ ∃ x_1, (toPermHom g) x_1 = 1 ∧ (Subgroup.centralizer {g}).subtype x_1 = x
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_2.e'_6
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ sign ((fun x ↦ ↑⟨c, hc⟩ ^ x) k) = 1

Tactic:
map_zpow

Goal state after:
case e'_2.e'_6
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ sign ↑⟨c, hc⟩ ^ k = 1
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case zero
n : ℕ
⊢ a 1 ^ 0 = a ↑0

Tactic:
rw [Nat.cast_zero]

Goal state after:
case zero
n : ℕ
⊢ a 1 ^ 0 = a 0
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image concatFn Finset.univ
w✝ : Fin r → ↥S
left✝ : w✝ ∈ Finset.univ
hx : concatFn w✝ ∈ T
c : ↥S
hnil : ↑c = []
⊢ [] ∈ ↑S

Tactic:
by simpa [hnil] using c.prop

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ⇑Kernel.id ∘ₘ μ = μ

Tactic:
by rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ (μ ⊗ₘ κ) (hμν.nullSet ×ˢ univ) = 0 ∧ (ν ⊗ₘ η) (hμν.nullSet ×ˢ univ)ᶜ = 0

Tactic:
rw [compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in hμν.nullSet, (κ a) univ ∂μ = 0 ∧ (ν ⊗ₘ η) (hμν.nullSetᶜ ×ˢ univ ∪ univ ×ˢ univᶜ) = 0
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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : StronglyMeasurable f
⊢ HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y ↦ f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Tactic:
simp only [hasFiniteIntegral_iff_enorm]
  rw [lintegral_compProd _ _ _ h1f.enorm]
  have : ∀ x, ∀ᵐ y ∂η (a, x), 0 ≤ ‖f (x, y)‖ := fun x => Eventually.of_forall fun y => norm_nonneg _
  simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
      (h1f.norm.comp_measurable measurable_prodMk_left).aestronglyMeasurable,
    enorm_eq_ofReal toReal_nonneg, ofReal_norm]
  have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
    rw [← and_congr_right_iff, and_iff_right_of_imp h1]
  rw [this]
  · intro h2f; rw [lintegral_congr_ae]
    filter_upwards [h2f] with x hx
    rw [ofReal_toReal]; finiteness
  · intro h2f; refine ae_lt_top ?_ h2f.ne; exact h1f.enorm.lintegral_kernel_prod_right''

Goal state after:
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 = 0

Tactic:
rw [Measure.tilted, integral_undef hf]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (rexp (f x) / 0)) = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_compProd : ∀ᵐ (x : 𝓧 × 𝓨) ∂ν ⊗ₘ η, μ.rnDeriv ν x.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
⊢ MeasurableSet {x | μ.rnDeriv ν x.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x}

Tactic:
simp only [measurableSet_setOfPred]

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_compProd : ∀ᵐ (x : 𝓧 × 𝓨) ∂ν ⊗ₘ η, μ.rnDeriv ν x.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
⊢ Measurable fun x ↦ μ.rnDeriv ν x.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ μ ≪ μ.tilted f

Tactic:
refine withDensity_absolutelyContinuous' ?_ ?_
    · exact (hf.1.aemeasurable.div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

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

Goal state before:
pp: case refine_2
α : 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}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | f x ≤ 0} ∩ s, f x ∂μ ≤ ∫ (x : α) in {x | g x ≤ 0} ∩ s, f x ∂μ

Tactic:
← Measure.restrict_restrict (hm _ h_meas_nonpos_g),

Goal state after:
case refine_2
α : 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}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | f x ≤ 0} ∩ s, f x ∂μ ≤ ∫ (x : α) in {x | g x ≤ 0}, f x ∂μ.restrict s
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ ⟪f - ↑((lpMeas E 𝕜 m 2 μ).orthogonalProjectionOnto f), g⟫ = 0

Tactic:
simp only [← Submodule.starProjection_apply,
    mem_lpMeas_iff_aestronglyMeasurable.mpr hg,
    Submodule.starProjection_inner_eq_zero f g]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
C : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
D : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∉ s n → f n x = 0
⊢ ∀ᵐ (a : X) ∂μ, ∑' (n : ι), ‖f n a‖ₑ < ∞

Tactic:
filter_upwards [C, D] with x hx h'x

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
C : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
D : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∉ s n → f n x = 0
x : X
hx : ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
h'x : ∀ (n : ι), x ∉ s n → f n x = 0
⊢ ∑' (n : ι), ‖f n x‖ₑ < ∞
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: case refine_2
α : 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 : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
h_add : P (f + g)
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
hgP' : P g
⊢ f + g =ᵐ[μ] ↑↑(toLp f hf_mem + toLp g hg_mem)

Tactic:
exact (hf_mem.coeFn_toLp.symm.add hg_mem.coeFn_toLp.symm).trans (Lp.coeFn_add _ _).symm

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] μ

pp: case pos
α : 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:
case pos
α : 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] μ
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ (∀ᵐ (x : 𝓧) ∂μ, Integrable (fun y ↦ log ((∂μ/∂ν) (x, y).1).toReal) (κ x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖log ((∂μ/∂ν) (x, y).1).toReal‖ ∂κ x) μ

Tactic:
simp only [ne_eq, enorm_ne_top, not_false_eq_true, integrable_const_enorm,
      Filter.eventually_true, integral_const, probReal_univ, smul_eq_mul, one_mul, true_and]
      rwa [← integrable_norm_iff (by fun_prop)] at h_int_μν

Goal state after: