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

Goal state before:
pp: case ind
n : ℕ
ih :
  ∀ m < n,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
⊢ ∀ {G : Type u} [inst : Group G] [Finite G],
    Nat.card G = n → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H

Tactic:
| ind n ih =>

Goal state after:
case ind
n : ℕ
ih :
  ∀ m < n,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
⊢ ∀ {G : Type u} [inst : Group G] [Finite G],
    Nat.card G = n → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
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)
⊢ ∀ (i : ι), MulAction.toEndHom.comp (φ i) = MulAction.toEndHom

Tactic:
by
    intro i
    simp only [MulAction.toEndHom, DFunLike.ext_iff, MonoidHom.coe_comp, MonoidHom.coe_mk,
      OneHom.coe_mk, comp_apply]
    intro h
    funext w
    apply NormalWord.ext_smul i
    simp only [summand_smul_def', equivPair, rcons, Word.equivPair_symm, Equiv.coe_fn_mk,
      Equiv.coe_fn_symm_mk, Word.equivPair_smul_same, Word.equivPair_tail_eq_inv_smul,
      Word.rcons_eq_smul, equiv_fst_eq_mul_inv, map_mul, map_inv, mul_smul, inv_smul_smul,
      smul_inv_smul, base_smul_def', MonoidHom.apply_ofInjective_symm]

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a b c : QuaternionGroup n), a * b * c = a * (b * c)

Tactic:
unfold instHMul

Goal state after:
n : ℕ
⊢ ∀ (a b c : QuaternionGroup n), a * b * c = a * (b * c)
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
⊢ commutator G < ⊤

Tactic:
have hp : p.Prime := Nat.minFac_prime Finite.one_lt_card.ne'

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
⊢ commutator G < ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
convert! Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))

Goal state after:
case e'_3
n : ℕ
hn : NeZero n
⊢ 4 = orderOf (xa 0)
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
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime ↑p)
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
g h : G
⊢ ϕ.symm g * ϕ.symm h = ϕ.symm (h * g)

Tactic:
mul_comm,

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
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime ↑p)
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
g h : G
⊢ ϕ.symm h * ϕ.symm g = ϕ.symm (h * g)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Nat.card α
⊢ Nontrivial ↥(alternatingGroup α)

Tactic:
refine nontrivial_of_three_le_card ?_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Nat.card α
⊢ 3 ≤ Nat.card α
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
⊢ ↑P ≤ Subgroup.center G ∨ ↑P ≤ commutator G

Tactic:
refine (commutator_eq_bot_or_commutator_eq_self P hK).imp (fun h ↦ ?_) (fun h ↦ ?_)

Goal state after:
case refine_1
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ⊥
⊢ ↑P ≤ Subgroup.center G

case refine_2
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ↑P ≤ commutator G
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ↑P ≤ commutator G

Tactic:
· rw [← h, commutator_def]
    exact Subgroup.commutator_mono le_top le_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
C : ℝ≥0∞
hC : C < ∞
hle : ∀ (a : α), (κ a) Set.univ ≤ C
⊢ κ.bound ≤ C

Tactic:
simp [bound, hle]

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

Goal state before:
pp: case inr
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
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ Function.Injective ⇑(f'.subgroupMap ↑P)

Tactic:
← MonoidHom.ker_eq_bot_iff,

Goal state after:
case inr
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
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ (f'.subgroupMap ↑P).ker = ⊥
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ hammingDist x x = 0

Tactic:
rw [hammingDist, card_eq_zero, filter_eq_empty_iff]

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ (∀ ⦃x_1 : ι⦄, x_1 ∈ univ → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1

Tactic:
mem_univ,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ (∀ ⦃x_1 : ι⦄, True → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ hammingDist x y ≤ hammingDist (fun i ↦ f i (x i)) fun i ↦ f i (y i)

Tactic:
dsimp [hammingDist]; gcongr; exact @hf _ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
⊢ Measurable fun a ↦ (κ a).restrict s

Tactic:
refine Measure.measurable_of_measurable_coe _ fun t ht => ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t✝ : Set β
κ : Kernel α β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable fun b ↦ ((κ b).restrict s) t
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
⊢ ∃ r ≥ 1, ↑r * ↑(S.sup List.length) < (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r

Tactic:
let K := ∑ w ∈ S, (1 / (Fintype.card α : ℝ)) ^ w.length

Goal state after:
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
⊢ ∃ r ≥ 1, ↑r * ↑(S.sup List.length) < (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ ((κ ∥ₖ η) x) s = ∫⁻ (b : β), (η x.2) (Prod.mk b ⁻¹' s) ∂κ x.1

Tactic:
rw [parallelComp_apply, Measure.prod_apply hs]

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

Goal state before:
pp: case pos.e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ ((κ ⊗ₖ η) a) (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a

Tactic:
Kernel.compProd_apply

Goal state after:
case pos.e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂κ a =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a

case pos.e_f.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ MeasurableSet (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s)
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 γ
b : β
⊢ sectL 0 b = 0

Tactic:
by simp [sectL]

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (x : Y), ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 ∂κ a.1 = ((κ ∥ₖ (ξ ∘ₖ η)) a) s

Tactic:
rw [parallelComp_apply, Measure.prod_apply hs]

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (x : Y), ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 ∂κ a.1 =
    ∫⁻ (x : Y), ((ξ ∘ₖ η) a.2) (Prod.mk x ⁻¹' s) ∂κ a.1
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ))

Tactic:
← comp_assoc,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = ξ ∘ₖ η ∥ₖ κ

Tactic:
← comp_assoc,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η ∘ₖ swap X' X) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X

Tactic:
← comp_assoc,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) ∘ₖ swap X' X = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
X' : Type u_5
Y' : Type u_6
Z' : Type u_7
mX' : MeasurableSpace X'
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X' Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ κ'))

Tactic:
← comp_assoc,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
X' : Type u_5
Y' : Type u_6
Z' : Type u_7
mX' : MeasurableSpace X'
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X' Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ (κ ∥ₖ κ')
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
Y' : Type u_6
Z' : Type u_7
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ' ∘ₖ copy X) = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')

Tactic:
← comp_assoc,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
Y' : Type u_6
Z' : Type u_7
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') ∘ₖ copy X = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: case pos.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) s ∂κ a = ((κ ⊗ₖ η) a) (Prod.snd ⁻¹' s)

Tactic:
Kernel.compProd_apply

Goal state after:
case pos.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) s ∂κ a = ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a

case pos.e_f.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ MeasurableSet (Prod.snd ⁻¹' s)
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
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂η (a, x) < ∞) →
    (∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂η (a, b) ∂κ a < ∞ ↔
      ∫⁻ (a_2 : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f (a_2, a)‖ₑ ∂η (a, a_2)).toReal ∂κ a < ∞)

Tactic:
intro h2f; rw [lintegral_congr_ae]
    filter_upwards [h2f] with x hx
    rw [ofReal_toReal]; finiteness

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:
mul_comm,

Goal state after:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ ENNReal.ofReal ((μ.real Set.univ)⁻¹ * (rexp c)⁻¹ * rexp c) = (μ Set.univ)⁻¹
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 (μ Set.univ)⁻¹.toReal = (μ Set.univ)⁻¹

Tactic:
ENNReal.ofReal_toReal

Goal state after:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ (μ Set.univ)⁻¹ = (μ Set.univ)⁻¹

case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ (μ Set.univ)⁻¹ ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
mul_comm,

Goal state after:
case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
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 γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) x) {p | p.1 ∈ s} = ∫⁻ (b : β), s.indicator (fun b ↦ (η (x, b)) Set.univ) b ∂κ x

Tactic:
Kernel.compProd_apply

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (x, b)) (Prod.mk b ⁻¹' {p | p.1 ∈ s}) ∂κ x =
    ∫⁻ (b : β), s.indicator (fun b ↦ (η (x, b)) Set.univ) b ∂κ x

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}
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
⊢ μ.rnDeriv (Measure.tilted 0 f) =ᶠ[⊥] fun x ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂0) * μ.rnDeriv 0 x

Tactic:
Filter.EventuallyEq

Goal state after:
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
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
⊢ llr (μ.tilted f) ν =ᵐ[μ] fun x ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

Tactic:
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

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 < ∞
⊢ llr (μ.tilted f) ν x = f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x