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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
obtain h | h | h := Nat.lt_trichotomy s.ncard sᶜ.ncard
  · exact isCoatom_stabilizer_of_ncard_lt_ncard_compl hs_nonempty h
  · contrapose hα
    rw [← Set.ncard_add_ncard_compl s, two_mul, ← h]
  · rw [← stabilizer_compl]
    apply isCoatom_stabilizer_of_ncard_lt_ncard_compl hsc_nonempty
    rwa [compl_compl]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
⊢ IsMultiplyPretransitive K α n

Tactic:
by_cases hn : n ≤ 2
    · apply MulAction.isMultiplyPretransitive_of_le' hn
      simp [← hα]
    · suffices (IsEmpty (Fin n ↪ α)) by infer_instance
      rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]

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 : S.Splitting
x✝¹ x✝ : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
⊢ (match ⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ with
    | ⟨n, g⟩ => S.inl n * s g) =
    (match ⟨n₁, g₁⟩ with
      | ⟨n, g⟩ => S.inl n * s g) *
      match ⟨n₂, g₂⟩ with
      | ⟨n, g⟩ => S.inl n * s g

Tactic:
by
    simp only [conjAct, MonoidHom.comp_apply, map_mul, inl_conjAct_comm, MonoidHom.coe_coe]
    group

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : IsPerfect G
⊢ ¬IsSolvable G

Tactic:
by
  intro h
  exact (h.commutator_lt_top_of_nontrivial G).ne commutator_eq_top

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn mn' : M × N
⊢ f (mn * mn').1 * g (mn * mn').2 = f mn.1 * g mn.2 * (f mn'.1 * g mn'.2)

Tactic:
by simpa using (comm _ _).mul_mul_mul_comm _ _

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : Cancels 1 w
⊢ (if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h
    else
      let g' := unitsSMulGroup φ d 1 (↑g • w).head;
      cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Tactic:
simp only [unitsSMulWithCancel, toSubgroup_one, id_eq, toSubgroup_neg_one, toSubgroupEquiv_one,
      group_smul_head, mul_inv_rev, dif_pos (this.2 hcan), dif_pos hcan]
    cases w using consRecOn
    · simp [Cancels] at hcan
    · simp only [smul_cons, consRecOn_cons]
      rw [← mul_smul, ← Subgroup.coe_mul, ← map_mul φ]
      rfl

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
z : α
hz : z ∈ {x | Equiv.swap x y ∈ closure S}
⊢ z ∈ orbit (↥(closure S)) x

Tactic:
exact orbit_eq_iff.mpr hf ▸ ⟨⟨swap z y, hz⟩, swap_apply_right z y⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
have hx'' : g.cycleOf x ∈ g.cycleFactorsFinset := hx' ▸ c.prop

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))
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
hH : H.Normal
g : Gᵐᵒᵖ
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩

Tactic:
let := H.fintypeQuotientOfFiniteIndex
  let ϕ : H →* H :=
    { toFun := fun h =>
        ⟨g.unop⁻¹ * h * g.unop,
          hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩
      map_one' := by rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
      map_mul' := fun h₁ h₂ => by
        simp only [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left] }
  refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm
  simp only [ϕ, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc,
    MonoidHom.id_apply, toPerm_symm_apply, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m ∧ sign g = 1
⊢ False

Tactic:
rcases hg with ⟨hg, hs⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : sign g = 1
⊢ False
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case pos
ι : 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
hep : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = i
⊢ ⟨i, (φ i) h * ⋯ ▸ (w.toList.head ⋯).snd⟩ ∈ w.toList.tail ∨
    w.toList.head? = some ⟨i, ⋯ ▸ (w.toList.head ⋯).snd⟩ ∨ ¬w.fstIdx = some i ∧ ⋯ ▸ (w.toList.head ⋯).snd = 1

pp: case neg
ι : 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
hep : ¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = i
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
· rcases hep with ⟨hnil, rfl⟩
        rw [head?_eq_some_head hnil]
        simp_all

Goal state after:
case neg
ι : 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
hep : ¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = i
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case neg
ι : 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
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
by_cases hw : w.toList = []

Goal state after:
case pos
ι : 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
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

case neg
ι : 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
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : ¬w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ #{g_1 | g_1.cycleType = g.cycleType} = Fintype.card { h // IsConj g h }

Tactic:
← Fintype.card_coe,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ Fintype.card ↥{g_1 | g_1.cycleType = g.cycleType} = Fintype.card { h // IsConj g h }
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ (2 ^ 2 * 3).factorization 2 = 4

Tactic:
Nat.factorization_mul_apply_of_coprime (by decide),

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ ((2 ^ 2).factorization 2 + (Nat.factorization 3) 2) = 4
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Nat.card ↥(kleinFour α) = 4

Tactic:
rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S, card_two_sylow_of_card_eq_four hα4 S]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent ↥(kleinFour α) = 1 ∨ Monoid.exponent ↥(kleinFour α) = 2
⊢ Monoid.exponent ↥(kleinFour α) = 2

Tactic:
apply Or.resolve_left this

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent ↥(kleinFour α) = 1 ∨ Monoid.exponent ↥(kleinFour α) = 2
⊢ ¬Monoid.exponent ↥(kleinFour α) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ ∀ (a : QuaternionGroup n), a.inv * a = 1

Tactic:
by
    rintro (i | i)
    · exact congr_arg a (neg_add_cancel i)
    · exact congr_arg a (sub_self (n + i))

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

Goal state before:
pp: 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
hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ (↑P).index

Tactic:
rw [(MonoidHom.ker_transferSylow_isComplement' P hP).index_eq_card]
    exact Subgroup.card_dvd_of_le (Abelianization.commutator_subset_ker _)

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 α β
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((0 ∘ₖ κ) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [comp_apply, FunLike.coe_zero]

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
⊢ (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r ≤ ↑r * ↑maxLen

Tactic:
let T : Finset (List α) := Finset.image concatFn (Finset.univ : Finset (Fin r → S))

Goal state after:
α : 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
⊢ (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r ≤ ↑r * ↑maxLen
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 α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ μ s✝ * (κ x✝) Set.univ = ((κ x✝) Set.univ • μ) s✝

Tactic:
Measure.smul_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ μ s✝ * (κ x✝) Set.univ = (κ x✝) Set.univ • μ s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : 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 δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h
    · simp only [map_zero]; infer_instance
    · have := IsMarkovKernel.map κ hf; infer_instance

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

Goal state before:
pp: 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)

Tactic:
exact hs.preimage (by fun_prop)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
simp [compProd_of_not_isSFiniteKernel _ _ hκ]

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

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

Tactic:
simp [compProd_of_not_isSFiniteKernel _ _ hκ]

Goal state after:
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 η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
by
  by_cases hκ : IsSFiniteKernel κ
  · refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
    rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)]
      at hs_zero ⊢
    filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero
  · simp [compProd_of_not_isSFiniteKernel _ _ hκ]

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

Goal state before:
pp: case pos.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
n : ℕ
x✝¹ : E
x✝ : x✝¹ ∈ (s n).range
⊢ Measurable fun x ↦ (κ x) (⇑(s n) ⁻¹' {x✝¹})

Tactic:
exact κ.measurable_coe ((s n).measurableSet_fiber _)

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

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

Tactic:
s

Goal state after:
case refine_1
α : 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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
⊢ ∀ (hs : MeasurableSet s),
    ∫⁻ (a : β × γ),
        (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0)) a ∂(κ ⊗ₖ η) a =
      ∫⁻ (a_1 : β),
        ∫⁻ (c_1 : γ),
          (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0))
            (a_1, c_1) ∂η (a, a_1) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind
α : 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✝ : β × γ → E
hE : CompleteSpace E
c : E
⊢ ∀ ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      ((κ ⊗ₖ η) a) s < ∞ →
        ∫ (z : β × γ), s.indicator (fun x ↦ c) z ∂(κ ⊗ₖ η) a =
          ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) (x, y) ∂η (a, x) ∂κ a

Tactic:
s

Goal state after:
case pos.h_ind
α : 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✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
⊢ MeasurableSet s →
    ((κ ⊗ₖ η) a) s < ∞ →
      ∫ (z : β × γ), s.indicator (fun x ↦ c) z ∂(κ ⊗ₖ η) a =
        ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) (x, y) ∂η (a, x) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos.e_f.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
b : β
⊢ MeasurableSet (Prod.mk b ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s)

Tactic:
exact hs.preimage (by fun_prop)

Goal state after:
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
h_eq : ∀ (b : β), (η (x, b)) {c | b ∈ s} = s.indicator (fun b ↦ (η (x, b)) Set.univ) b
⊢ ∫⁻ (b : β), (η (x, b)) {x | b ∈ s} ∂κ x = ∫⁻ (b : β), s.indicator (fun b ↦ (η (x, b)) Set.univ) b ∂κ x

Tactic:
h_eq

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

Goal state before:
pp: case pos.h_ind
α : 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✝ : γ → E
hE : CompleteSpace E
c : E
⊢ ∀ ⦃s : Set γ⦄,
    MeasurableSet s →
      ((η ∘ₖ κ) a) s < ∞ →
        ∫ (z : γ), s.indicator (fun x ↦ c) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) y ∂η x ∂κ a

Tactic:
s

Goal state after:
case pos.h_ind
α : 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✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
⊢ MeasurableSet s →
    ((η ∘ₖ κ) a) s < ∞ →
      ∫ (z : γ), s.indicator (fun x ↦ c) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) y ∂η x ∂κ a
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:
by
  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: