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

Goal state before:
pp: case hs
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
ha : a ∈ s
g : M
hg : g ∈ stabilizer M s
hb : g • a ∈ s
⊢ ∃ g_1, g_1 • a = g • a

Tactic:
exact ⟨⟨g, hG.le hg⟩, rfl⟩

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

Goal state before:
pp: case hs'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
ha : a ∈ sᶜ
g : M
hg : g ∈ stabilizer M s
hb : g • a ∈ sᶜ
⊢ ∃ g_1, g_1 • a = g • a

Tactic:
exact ⟨⟨g, hG.le hg⟩, rfl⟩

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective toPerm
this : IsPreprimitive ↥(stabilizer M s) ↑s
φ' : ↥(stabilizer M s) → M := Subtype.val
f' : ↑s →ₑ[φ'] α := { toFun := Subtype.val, map_smul' := ⋯ }
⊢ IsBlock (↥(stabilizer M s)) (Subtype.val ⁻¹' B)

Tactic:
exact hB.preimage f'

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝⁴ : Group N
inst✝³ : Group E
inst✝² : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝¹ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
E'' : Type u_5
inst✝ : Group E''
S'' : GroupExtension N E'' G
equiv' : S'.Equiv S''
⊢ ⇑(equiv.trans equiv'.toMulEquiv) ∘ ⇑S.inl = ⇑S''.inl

Tactic:
by rw [MulEquiv.coe_trans, Function.comp_assoc, equiv.inl_comm, equiv'.inl_comm]

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = (σ' g)⁻¹ * σ g
⊢ σ g = σ' g * ((σ' g)⁻¹ * σ g)

Tactic:
mul_inv_cancel_left

Goal state after:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = (σ' g)⁻¹ * σ g
⊢ σ g = σ g
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

Tactic:
by
        obtain ⟨e, he⟩ := r_iff_exists.1 hab
        obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
        simp only [mul_right_inj] at he hf
        rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_le_mul_iff_right, ← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_le_mul_iff_left]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
rw [← eq₂, (f.map_units s₂).dvd_mul_right] at this

Goal state after:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ n₂
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
⊢ ∃ g, g.cycleType = m

Tactic:
use List.prod (List.map (fun l => List.formPerm l) p)

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
⊢ (List.map (fun l ↦ l.formPerm) p).prod.cycleType = m
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
⊢ Fintype.card { a // φ a = i } = Fintype.card { a // f a = ↑i }

Tactic:
apply Fintype.card_congr

Goal state after:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
⊢ { a // φ a = i } ≃ { a // f a = ↑i }
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a✝ b✝ : Perm ↥g.cycleFactorsFinset
hσ : a✝ ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}
hτ : b✝ ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}
⊢ a✝ * b✝ ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}

Tactic:
by
    simp only [Subtype.forall, Set.mem_ofPred_eq, coe_mul, Function.comp_apply]
    simp only [Subtype.forall, Set.mem_ofPred_eq] at hσ hτ
    intro c hc
    rw [hσ, hτ]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
⊢ ⟨a.ofPermHom 1, ⋯⟩ = 1

Tactic:
by simp only [map_one, mk_eq_one]

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

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

Tactic:
eq_comm,

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op (g₁ * g₂)⁻¹ • α) T = (fun α ↦ op g₁⁻¹ • α) ((fun α ↦ op g₂⁻¹ • α) T)

Tactic:
mul_inv_rev

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op (g₂⁻¹ * g₁⁻¹) • α) T = (fun α ↦ op g₁⁻¹ • α) ((fun α ↦ op g₂⁻¹ • α) T)
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ β✝ : H.QuotientDiff
β α : H.LeftTransversal
⊢ diff (MonoidHom.id ↥H) β α * ((powCoprime hH).symm (diff (MonoidHom.id ↥H) β α))⁻¹ ^ H.index = 1

Tactic:
by rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel]

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

Goal state before:
pp: case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ _root_.Disjoint (↑a).support (↑b).support

Tactic:
← disjoint_iff_disjoint_support

Goal state after:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ (↑a).Disjoint ↑b
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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
h7 : Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G
⊢ ∃ H, N.IsComplement' H

Tactic:
have h8 : (Nat.card N).Coprime (Nat.card (H.map K.subtype)) := by
    rwa [hH]

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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
h7 : Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G
h8 : (Nat.card ↥N).Coprime (Nat.card ↥(map K.subtype H))
⊢ ∃ H, N.IsComplement' H
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card ↥(kleinFour α) ≠ 0

Tactic:
rw [kleinFour_card_of_card_eq_four hα4]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ 4 ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ (↑g).support ∈ Set.powersetCard α 4

Tactic:
simp [← sum_cycleType, hg]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

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

Tactic:
eq_comm,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 ↔ x = y
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (κ a) (univ \ (Prod.mk a ⁻¹' t ∩ univ)) = (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)

Tactic:
Set.inter_univ,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (κ a) (univ \ Prod.mk a ⁻¹' t) = (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
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 α β
⊢ 0 ∘ₖ κ = 0

Tactic:
ext; simp [comp_apply, FunLike.coe_zero]

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

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
n : ℕ
⊢ (Measure.comap f ((κ.seq n) a)) t = ((κ.seq n) a) (f '' t)

Tactic:
Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht

Goal state after:
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
n : ℕ
⊢ ((κ.seq n) a) (f '' t) = ((κ.seq n) a) (f '' t)
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 α (β × γ)
h : IsFiniteKernel κ.fst
a : α
⊢ (κ a) Set.univ ≤ (κ.fst a) Set.univ

Tactic:
rw [fst_apply' _ _ MeasurableSet.univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
a : α
⊢ (κ a) Set.univ ≤ (κ a) {p | p.1 ∈ Set.univ}
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 α β
f : β → γ
g : β → δ
hg : Measurable g
hf : ¬Measurable f
⊢ ¬Measurable fun x ↦ (f x, g x)

Tactic:
contrapose hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable fun x ↦ (f x, g x)
⊢ Measurable f
Module: Mathlib.Probability.Kernel.Composition.MapComap

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 (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
a✝ : MeasurableSet s
⊢ (((κ.sectR a).comap f hf) d) s = ((κ.comap (fun d ↦ (a, f d)) ⋯) d) s

Tactic:
rw [comap_apply, sectR_apply, comap_apply]

Goal state after:
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) ∘ₖ (κ ∥ₖ κ')

Tactic:
comp_id

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 η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∥ₖ η' ∘ₖ (κ ∥ₖ κ')
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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ η ∥ₖ κ = η ∘ₖ Kernel.id ∥ₖ κ

Tactic:
comp_id

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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ η ∥ₖ κ = η ∥ₖ κ
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ = ⇑η ∘ₘ map Prod.snd (μ ⊗ₘ κ)

Tactic:
← deterministic_comp_eq_map measurable_snd,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ = ⇑η ∘ₘ ⇑(Kernel.deterministic Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ = ⇑(η ∘ₖ Kernel.deterministic Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ

Tactic:
Kernel.comp_deterministic_eq_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ = ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ
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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
a✝ : β
h2f : Integrable (fun y ↦ f (a✝, y)) (η (a, a✝))
h2g : Integrable (fun y ↦ g (a✝, y)) (η (a, a✝))
⊢ F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂η (a, a✝))

Tactic:
simp [integral_sub h2f h2g]

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)
a✝ : β
h2f : Integrable (fun y ↦ f (a✝, y)) (η (a, a✝))
h2g : Integrable (fun y ↦ g (a✝, y)) (η (a, a✝))
⊢ F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂η (a, a✝))

Tactic:
simp [integral_sub h2f h2g]

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

Goal state before:
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.AbsolutelyContinuous.rfl

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) ∂μ) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ = 1

Tactic:
← ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ fun _ ↦ (exp_pos _).le),

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ = 1
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✝ : IsFiniteKernel η
a : α
⊢ ((κ ⊗ₖ η) a) Set.univ ≤ (κ a) Set.univ * η.bound

Tactic:
by_cases hκ : IsSFiniteKernel κ
  swap
  · rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]
    simp
  rw [compProd_apply .univ]
  let Cη := η.bound
  calc
    ∫⁻ b, η (a, b) Set.univ ∂κ a ≤ ∫⁻ _, Cη ∂κ a :=
      lintegral_mono fun b => measure_le_bound η (a, b) Set.univ
    _ = Cη * κ a Set.univ := MeasureTheory.lintegral_const Cη
    _ = κ a Set.univ * Cη := mul_comm _ _

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 α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)

Tactic:
simp [integral_sub h2f h2g]

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 α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)

Tactic:
simp [integral_sub h2f h2g]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ -llr μ ν =ᵐ[μ] llr ν μ

Tactic:
filter_upwards [Measure.inv_rnDeriv hμν] with x hx
  rw [Pi.neg_apply, llr, llr, ← log_inv, ← ENNReal.toReal_inv]
  congr

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

Goal state before:
pp: case hx
α : 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 < ∞
⊢ c.toReal ≠ 0

Tactic:
ENNReal.toReal_ne_zero

Goal state after:
case hx
α : 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 < ∞
⊢ c ≠ 0 ∧ c ≠ ∞