mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ rcons i { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } =
      rcons i { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ } →
    { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } =
      { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ }

Tactic:
simp only [rcons, NormalWord.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
    Word.Pair.mk.injEq, Pair.mk.injEq, and_imp]

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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2 →
    tail₁ = tail₂ → (⋯.equiv head₁).1 = (⋯.equiv head₂).1 → head₁ = head₂ ∧ tail₁ = tail₂
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 2 = a ↑n

Tactic:
by simp [sq]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
⊢ IsCyclic ↥↑P

Tactic:
have := Fact.mk hp

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this✝ : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
⊢ IsCyclic ↥↑P

Tactic:
have := Fact.mk hp

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P
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
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
⊢ commutator G < ⊤

Tactic:
have := Fact.mk hp

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ commutator G < ⊤
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Tactic:
have := Fact.mk hp

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p
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)
g : PushoutI φ
⊢ (fun w ↦ w.prod) ((fun g ↦ g • empty) g) = g

Tactic:
simp only [prod_smul, prod_empty, mul_one]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
have := Fact.mk hp

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
h_cop : (Nat.card G).Coprime (Nat.card G'')
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
⊢ IsCyclic ↥↑P

Tactic:
have := Fact.mk hp

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
h_cop : (Nat.card G).Coprime (Nat.card G'')
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η : Kernel α β
inst✝ : IsEmpty β
κ : Kernel α β
⊢ κ = 0 ∨ IsMarkovKernel κ

Tactic:
by
    left
    ext a s
    simp [Set.eq_empty_of_isEmpty s]

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

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

Tactic:
Measure.lintegral_bind (Kernel.aemeasurable _) hg.aemeasurable

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a : β), ∫⁻ (x : γ), g x ∂η a ∂κ a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a
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
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc r (r * maxLen)
D : ℝ := ↑(Fintype.card α)
⊢ (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r = ∑ w, ∏ i, (1 / D) ^ (↑(w i)).length

Tactic:
by
      simpa [(Finset.sum_coe_sort S _).symm] using
        Fintype.sum_pow (f := fun c : S => (1 / D) ^ c.val.length) r

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ const β μ ∘ₖ κ = const α μ

Tactic:
by
  ext; simp_rw [const_comp, measure_univ, one_smul, const_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ (∫⁻ (b : β), (η b) s✝ ∂Measure.sum fun n ↦ (κ n) a✝) = ∑' (i : ι), ((η ∘ₖ κ i) a✝) s✝

Tactic:
lintegral_sum_measure,

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 : ι), ∫⁻ (b : β), (η b) s✝ ∂(κ i) a✝ = ∑' (i : ι), ((η ∘ₖ κ i) a✝) s✝
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case refine_1
α : 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 : ℕ
⊢ ∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s),
    Measurable fun a ↦
      ∫⁻ (b : β), (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0)) (a, b) ∂κ a

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 c t ht
    simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
    exact Kernel.measurable_lintegral_indicator_const (κ := κ) ht c

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 : ℕ
⊢ ∀ ⦃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
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : IsSFiniteKernel η
⊢ 0 ∥ₖ η = 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ 0 ∥ₖ η = 0

Tactic:
· ext; simp [parallelComp_apply]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ 0 ∥ₖ η = 0
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0

Tactic:
· ext; simp [parallelComp_apply]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun x ↦
    ∫⁻ (y : β),
      ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β))
          (x, y))
        s ∂κ (a, a).2

Tactic:
suffices Measurable fun p : α × β ↦
      (swap γ β ∘ₖ (η ∥ₖ Kernel.id)
        ∘ₖ deterministic MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _)
        ∘ₖ (Kernel.id ∥ₖ copy β)) p s by fun_prop

Goal state after:
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun p ↦
    ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β)) p) s
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ×ₖ κ) ∘ₘ μ

Tactic:
by
  rw [compProd, Kernel.compProd_prodMkLeft_eq_comp]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ (⇑κ + ⇑η) ∘ₘ μ = ⇑κ ∘ₘ μ + ⇑η ∘ₘ μ

Tactic:
by rw [← FunLike.coe_add, add_comp]

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

Goal state before:
pp: case refine_2.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f✝ : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f✝)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f✝)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f✝ a b
h_mono : Monotone F
this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, (F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), (F n) (b, c) ∂η (a, b)
h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b ↦ ∫⁻ (c : γ), f' (b, c) ∂η (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑f')
hf_eq : ∫⁻ (a : β × γ), f a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f (a_1, c) ∂η (a, a_1) ∂κ a
hf'_eq : ∫⁻ (a : β × γ), f' a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f' (a_1, c) ∂η (a, a_1) ∂κ a
⊢ Measurable fun a_1 ↦ ∫⁻ (c : γ), f (a_1, c) ∂η (a, a_1)

Tactic:
exact h_some_meas_integral f

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ ν ⊗ₘ η ≪ ν ⊗ₘ η

Tactic:
· exact Measure.MutuallySingular.compProd_of_left (μ.mutuallySingular_singularPart _) _ _

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ ν ⊗ₘ η ≪ ν ⊗ₘ η
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ μ.tilted f = μ.withDensity fun x ↦ ↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯)

Tactic:
rw [Measure.tilted]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) =
    μ.withDensity fun x ↦ ↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯)
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ 0 ≤ᵐ[μ.restrict s] fun a ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact ae_of_all _ (fun _ ↦ by positivity)

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

Goal state before:
pp: case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ 0 ≤ᵐ[μ.restrict s] fun a ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact ae_of_all _ (fun _ ↦ by positivity)

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
have hf' : ¬ Integrable (fun x ↦ exp (f x)) μ := by
      exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
have hf' : ¬ Integrable (fun x ↦ exp (f x)) μ := by
      exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ (∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂Measure.sum fun n ↦ (κ n) a) = (Measure.sum fun n ↦ (κ n ⊗ₖ η) a) s

Tactic:
lintegral_sum_measure,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∑' (i : ι), ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂(κ i) a = (Measure.sum fun n ↦ (κ n ⊗ₖ η) a) s
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
have hf' : ¬ Integrable (fun x ↦ exp (f x)) μ := by
      exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
have hf' : ¬ Integrable (fun x ↦ exp (f x)) μ := by
      exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᵐ[ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
rw [ENNReal.toReal_ne_zero]
    simp [hx_pos.ne', hx_ne_top.ne]

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

Goal state before:
pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
rw [ENNReal.toReal_ne_zero]
    simp [hx_pos.ne', hx_ne_top.ne]

Goal state after:
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 ν
⊢ llr (μ.tilted f) ν =ᵐ[μ] fun x ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

Tactic:
cases eq_zero_or_neZero μ with
  | inl hμ =>
    simp only [hμ, ae_zero, Filter.EventuallyEq, Filter.eventually_bot]
  | inr h0 =>
    filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_left μ hfν), Measure.rnDeriv_pos hμν,
      hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top
    rw [llr, hx, log_mul, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr,
      ← sub_eq_add_neg]
    · simp only [ne_eq, inv_eq_zero]
      exact (integral_exp_pos hf).ne'
    · simp only [ne_eq, div_eq_zero_iff]
      push Not
      exact ⟨(exp_pos _).ne', (integral_exp_pos hf).ne'⟩
    · simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
hfν : Integrable (fun x ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ -f x + log (∫ (x : α), rexp (f x) ∂ν)) μ

Tactic:
exact hfμ.neg.add (integrable_const _)

Goal state after: