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'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup ↥N
inst✝ : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
| map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N

Tactic:
rhs
    rhs
    rw [← N.range_subtype, N.subtype.range_eq_map]

Goal state after:
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'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup ↥N
inst✝ : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
| map N.subtype ⊤
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ #{g | g.cycleType = {n}} = (n - 1)! * (card α).choose n

Tactic:
have aux : n ! = (n - 1)! * n := by rw [mul_comm, mul_factorial_pred hn₀]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ #{g | g.cycleType = {n}} = (n - 1)! * (card α).choose n
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
hg0 : 4 ≠ 2
t : Multiset ℕ
h1 : (4 ::ₘ t).sum ≤ 4
ht : g.cycleType = 4 ::ₘ t
⊢ (-1) ^ (g.cycleType.sum + g.cycleType.card) ≠ 1

Tactic:
Multiset.sum_cons,

Goal state after:
case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
hg0 : 4 ≠ 2
t : Multiset ℕ
h1 : 4 + t.sum ≤ 4
ht : g.cycleType = 4 ::ₘ t
⊢ (-1) ^ (g.cycleType.sum + g.cycleType.card) ≠ 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
w : NormalWord d
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
⊢ motive w

Tactic:
rcases w with ⟨w, head, h3⟩

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i
⊢ motive { toWord := w, head := head, normalized := h3 }
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i

Tactic:
exact congr_arg xa (sub_zero i)

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

Goal state after:
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
g : ↥(alternatingGroup α)
hk22 : ∃ c, c * ↑k * c⁻¹ = ↑g
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
⊢ commutator G < ⊤

Tactic:
by
  let p := (Nat.card G).minFac
  have hp : p.Prime := Nat.minFac_prime Finite.one_lt_card.ne'
  have := Fact.mk hp
  let P : Sylow p G := default
  have hP := isZGroup p hp P
  let f := MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)
  refine lt_of_le_of_lt (Abelianization.commutator_subset_ker f) ?_
  have h := P.ne_bot_of_dvd_card (Nat.card G).minFac_dvd
  contrapose h
  rw [← Subgroup.isComplement'_top_left, ← (not_lt_top_iff.mp h)]
  exact hP.isComplement' rfl

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)
w : NormalWord d
⊢ w.prod • empty = w

Tactic:
induction w using consRecOn with
  | empty => simp
  | cons i g w _ _ _ _ ih =>
    rw [prod_cons, mul_smul, ih, cons_eq_smul]
  | base h w _ ih =>
    rw [prod_smul, mul_smul, ih]

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

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h :
  commutator ↥(Subgroup.normalizer ↑⁅commutator ↥H, commutator ↥H⁆) ≤
    ⁅commutator ↥H, commutator ↥H⁆.normalizerMonoidHom.ker
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
Subgroup.normalizerMonoidHom_ker,

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h :
  commutator ↥(Subgroup.normalizer ↑⁅commutator ↥H, commutator ↥H⁆) ≤
    (Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆).subgroupOf
      (Subgroup.normalizer ↑⁅commutator ↥H, commutator ↥H⁆)
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
⊢ map 0 f = 0

Tactic:
by
  ext
  by_cases hf : Measurable f
  · simp [map_apply, hf]
  · simp [map_of_not_measurable _ hf]

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 α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ (Measure.sum fun n ↦ ((κ.seq n).map f) a) s = ((κ.map f) a) s

Tactic:
map_apply' κ hf a hs,

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ (Measure.sum fun n ↦ ((κ.seq n).map f) a) s = (κ a) (f ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, κ a = 0
⊢ μ ⊗ₘ κ = μ ⊗ₘ 0

Tactic:
exact compProd_congr h

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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel κ.fst

Tactic:
by rw [Kernel.fst_eq]; infer_instance

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✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : α × α), ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η) b ∂(copy α) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a

Tactic:
copy_apply

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : α × α), ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η) b ∂Measure.dirac (a, a) = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
Module: Mathlib.Probability.Kernel.Composition.Prod

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (a : β × δ), f a.swap ∂(prodMkRight γ κ ×ₖ prodMkLeft α η) x

Tactic:
lintegral_prod

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (b, c).swap ∂(prodMkLeft α η) x ∂(prodMkRight γ κ) x

case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

Tactic:
· simp [compProd_of_not_isSFiniteKernel_right _ _ hη]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case pos
α : 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) (κ x)
⊢ Tendsto (fun i ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂κ x))

Tactic:
have (n : _) : Integrable (s' n x) (κ x) := by
        apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
        filter_upwards with y
        simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
      simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_ofPred_eq]
      refine
        tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
          (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_
      · -- Porting note: was
        -- exact fun n => Eventually.of_forall fun y =>
        --   SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
        exact fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n
      · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) ?_
        apply subset_closure
        simp [-uncurry_apply_pair]

Goal state after:
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 η
inst✝ : NormedSpace ℝ E
f g : β × γ → E
F : E → ℝ≥0∞
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
⊢ ∫⁻ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a =
    ∫⁻ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a

Tactic:
refine lintegral_congr_ae ?_
  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
  simp [integral_sub h2f h2g]

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

Goal state before:
pp: case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) = (μ Set.univ)⁻¹

Tactic:
div_eq_mul_inv,

Goal state after:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ ENNReal.ofReal (rexp c * (μ.real Set.univ * rexp c)⁻¹) = (μ Set.univ)⁻¹
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
by_cases hf : Integrable (fun x ↦ exp (f x)) μ
  · rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal]
    · exact hf.integrableOn.div_const _
    · exact ae_of_all _ (fun _ ↦ by positivity)
  · simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.coe_zero,
      Pi.zero_apply, integral_undef hf, div_zero, integral_zero, ENNReal.ofReal_zero]

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
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
neg_eq_iff_eq_neg

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.Tilted

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ ((μ.tilted f).tilted g) s = (μ.tilted (f + g)) s

Tactic:
rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, setLIntegral_tilted' f _ hs]

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s,
      ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) ∂μ =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp ((f + g) a) / ∫ (x : α), rexp ((f + g) x) ∂μ) ∂μ
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ ENNReal.ofReal (rexp (-f x) / (∫ (x : α), rexp (f x) ∂ν)⁻¹) = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)

pp: case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
div_eq_mul_inv,

Goal state after:
case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ ENNReal.ofReal (rexp (-f x) * (∫ (x : α), rexp (f x) ∂ν)⁻¹⁻¹) =
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)

case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ log (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) + log (μ.rnDeriv ν x).toReal =
    f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

pp: case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0

pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ log (rexp (f x) * (∫ (x : α), rexp (f x) ∂μ)⁻¹) + log (μ.rnDeriv ν x).toReal =
    f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0

case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ klFun 0 = 1

Tactic:
by simp [klFun]

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

Goal state before:
pp: ⊢ klFun 1 = 0

Tactic:
by simp [klFun]

Goal state after:
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
h_llr_smul_inv : llr (c⁻¹ • μ) ν =ᵐ[μ] llr μ (c • ν)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + ↑c * ν.real univ - μ.real univ =
    ↑c * ((↑c)⁻¹ * ∫ (a : α), llr μ (c • ν) a ∂μ + ν.real univ - (↑c)⁻¹ * μ.real univ)

Tactic:
mul_sub,

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
h_llr_smul_inv : llr (c⁻¹ • μ) ν =ᵐ[μ] llr μ (c • ν)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + ↑c * ν.real univ - μ.real univ =
    ↑c * ((↑c)⁻¹ * ∫ (a : α), llr μ (c • ν) a ∂μ + ν.real univ) - ↑c * ((↑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 : ↥(Lp E' 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
hf_meas : AEStronglyMeasurable (↑↑f) μ
⊢ ↑↑f =ᵐ[μ] 0

Tactic:
by
  let f_meas : lpMeas E' 𝕜 m p μ := ⟨f, hf_meas⟩
  have hf_f_meas : f =ᵐ[μ] f_meas := by simp [f_meas]
  refine hf_f_meas.trans ?_
  exact lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero
    hm f_meas hp_ne_zero hp_ne_top hf_int_finite hf_zero

Goal state after: