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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
⊢ h = 1

Tactic:
by_contra hh1

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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0

Tactic:
(card_of_cycleType_eq_zero_iff α).mpr hm,

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ 0 * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0
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
| N

Tactic:
← N.range_subtype,

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
| N.subtype.range
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card ↥N * N.index ≠ 0

Tactic:
exact mul_ne_zero hN1 hN2

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

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : (↑(orderOf (a 1))).val = 0
⊢ False

Tactic:
ZMod.val_natCast,

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : orderOf (a 1) % (2 * n) = 0
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Tactic:
have h1 : Abelianization G ≃* H := hH.symm.QuotientMulEquiv

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
h1 : Abelianization G ≃* ↥H
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)
Module: Mathlib.InformationTheory.Hamming

Goal state before:
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:
rintro ⟨_, hε, hs⟩ ⟨_, _⟩ rfl
      refine hs (lt_of_eq_of_lt ?_ hε)
      exact mod_cast hammingDist_self _

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

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' f i)
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' ⋃ i, f i)

Tactic:
| iUnion f h_disj hf_meas hf =>

Goal state after:
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:
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.InformationTheory.Coding.KraftMcMillan

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

Tactic:
simp at *

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

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

Tactic:
simp at *

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

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

Tactic:
simp at *

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

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

Tactic:
simp at *

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

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

Tactic:
simp at *

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

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

Tactic:
simp at *

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

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

Tactic:
simp at *

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

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

Tactic:
simp at *

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
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

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

Tactic:
simp at *

Goal state after:
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.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (η ∘ₖ κ)

Tactic:
by
  simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, comp_sum_left, comp_sum_right]
  infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst✝ : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ μ ⊗ₘ Kernel.sum κ = sum fun i ↦ μ ⊗ₘ κ i

Tactic:
rw [compProd, ← Kernel.sum_prodMkLeft, Kernel.compProd_sum_right]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst✝ : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ (Kernel.sum fun i ↦ Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ i)) () = sum fun i ↦ μ ⊗ₘ κ i
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
rw [compProd, Kernel.setLIntegral_compProd _ _ _ hf hs ht]
  simp

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 α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in s, (η a) univ ∂ν = 0

Tactic:
exact setLIntegral_measure_zero _ _ hs0

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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : α), IsMarkovKernel (κ.sectR b)
x✝ : α × β
⊢ (κ x✝) Set.univ = 1

Tactic:
rw [← sectR_apply, measure_univ]

Goal state after:
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 γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0

Tactic:
· ext a s hs
    rw [Kernel.compProd_apply hs]
    simp

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

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

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

Tactic:
· ext a s hs
    rw [Kernel.compProd_apply hs]
    simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
⊢ ((κ ⊗ₖ η) x) (Prod.fst ⁻¹' s) = (κ x) s

Tactic:
compProd_apply (measurable_fst hs),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
⊢ ∫⁻ (b : β), (η (x, b)) (Prod.mk b ⁻¹' Prod.fst ⁻¹' s) ∂κ x = (κ x) s
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 γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
μ : Measure δ
inst✝ : SFinite μ
⊢ η ×ₖ const β μ ∘ₖ κ = η ∘ₖ κ ×ₖ const α μ

Tactic:
ext x s ms
  simp_rw [comp_apply' _ _ _ ms, prod_apply' _ _ _ ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_left ms)]

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

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

Tactic:
change
    StronglyMeasurable
      ((fun y => ∫ x, (fun u : γ × α × β => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable ((fun y ↦ ∫ (x : γ), (fun u ↦ f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x ↦ (a, x))
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_2
α : 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
⊢ ∫⁻ (x : β × γ), f x + f' x ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) + f' (b, c) ∂η (a, b) ∂κ a

Tactic:
lintegral_add_left (SimpleFunc.measurable _),

Goal state after:
case refine_2
α : 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
⊢ ∫⁻ (a : β × γ), f a ∂(κ ⊗ₖ η) a + ∫⁻ (a : β × γ), f' a ∂(κ ⊗ₖ η) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) + f' (b, c) ∂η (a, b) ∂κ a
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
by
  cases eq_zero_or_neZero μ with
  | inl h => rw [h]; simp
  | inr h0 =>
    rw [integral_tilted f]
    simp_rw [smul_eq_mul]
    have : ∀ x, (exp (f x) / ∫ x, exp (f x) ∂μ) * exp (g x)
        = (exp ((f + g) x) / ∫ x, exp (f x) ∂μ) := by
      intro x
      rw [Pi.add_apply, exp_add]
      ring
    simp_rw [this, div_eq_mul_inv]
    rw [integral_mul_const]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
⊢ llr (c⁻¹ • μ) ν =ᵐ[μ] llr μ (c • ν)

Tactic:
have hc_ne_top' : c⁻¹ ≠ ∞ := by simp [hc]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
hc_ne_top' : c⁻¹ ≠ ∞
⊢ llr (c⁻¹ • μ) ν =ᵐ[μ] llr μ (c • ν)
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
⊢ Integrable g (μ.tilted f) ↔ Integrable (fun x ↦ rexp (f x) • g x) μ

Tactic:
by
  by_cases hμ : μ = 0
  · simp [hμ]
  have hf_meas : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
  rw [Measure.tilted, integrable_withDensity_iff_integrable_smul₀' (by fun_prop) (by simp)]
  calc Integrable (fun x ↦ (ENNReal.ofReal (exp (f x) / ∫ a, exp (f a) ∂μ)).toReal • g x) μ
  _ ↔ Integrable (fun x ↦ (exp (f x) / ∫ a, exp (f a) ∂μ) • g x) μ := by
    congr! with a
    rw [ENNReal.toReal_ofReal]
    positivity
  _ ↔ Integrable (fun x ↦ (∫ a, exp (f a) ∂μ)⁻¹ • exp (f x) • g x) μ := by
    congr! 2 with a
    rw [smul_smul, div_eq_inv_mul]
  _ ↔ Integrable (fun x ↦ exp (f x) • g x) μ := by
    rw [integrable_fun_smul_iff]
    simp only [ne_eq, inv_eq_zero]
    have : NeZero μ := ⟨hμ⟩
    exact (integral_exp_pos hf).ne'

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h : ν = 0
⊢ ∀ᶠ (x : α) in ⊥,
    μ.rnDeriv (Measure.tilted 0 f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂0) * μ.rnDeriv 0 x

Tactic:
exact Filter.eventually_bot

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : ¬c = 0
x : α
hx : (c • μ).rnDeriv (c • ν) x = μ.rnDeriv ν x
⊢ log ((↑c • μ).rnDeriv (↑c • ν) x).toReal = log (μ.rnDeriv ν x).toReal

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
⊢ llr (c • μ) (c • ν) =ᵐ[μ] llr μ ν

Tactic:
simp_rw [← Measure.coe_nnreal_smul]
  filter_upwards [llr_smul_same hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx
  rw [hx]

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : Integrable (fun x ↦ rexp (f x)) μ
h : μ = 0
⊢ ∀ᶠ (x : α) in ⊥, log ((Measure.tilted 0 f).rnDeriv 0 x).toReal = f x - log (∫ (x : α), rexp (f x) ∂0)

Tactic:
exact Filter.eventually_bot

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

Goal state before:
pp: ⊢ Tendsto (fun x ↦ derivWithin klFun (Ioi x) x) atTop atTop

Tactic:
simp only [rightDeriv_klFun]
  exact tendsto_log_atTop

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f : ∀ (s : Set α), MeasurableSet s → 0 < μ s → ∞ ≤ μ s
fn : ℕ → SimpleFunc α E
hfn : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) < ∞
hfn_lim : ∀ (x : α), Tendsto (fun n ↦ (fn n) x) atTop (𝓝 (f x))
A : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) = 0
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), (fn n) x = 0
x : α
hx : ∀ (n : ℕ), (fn n) x = 0
⊢ Tendsto (fun n ↦ (fn n) x) atTop (𝓝 (0 x))

Tactic:
simp [hx]

Goal state after: