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

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ 2 * 3 ≤ 2 * Nat.card ↥G

Tactic:
simp only [mul_le_mul_iff_right₀, Nat.succ_pos]

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ 3 ≤ Nat.card ↥G
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
u' : ℤˣ
g' : G
h' : u' = u ∧ g' = w.head ∨ (u', g') ∈ w.toList
⊢ g' ∈ d.set u'

Tactic:
rcases h' with ⟨rfl, rfl⟩ | h'

Goal state after:
case inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
w : NormalWord d
u' : ℤˣ
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
⊢ w.head ∈ d.set u'

case inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
u' : ℤˣ
g' : G
h' : (u', g') ∈ w.toList
⊢ g' ∈ d.set u'
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
⊢ ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α

Tactic:
intro l hl n hn

Goal state after:
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ n < Fintype.card α
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
a a' : g.Basis
x✝ : (fun a ↦ a.toFun) a = (fun a ↦ a.toFun) a'
⊢ a = a'

Tactic:
by cases a; cases a'; congr

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hc hm]

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑τ c)) ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ 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
α β : H.LeftTransversal
h : { r := fun α β ↦ diff (MonoidHom.id ↥H) α β = 1, iseqv := ⋯ } α β
⊢ ↑(diff (MonoidHom.id ↥H) (op g⁻¹ • α) (op g⁻¹ • β)) = ↑1

Tactic:
rwa [smul_diff_smul', coe_mk, coe_one, mul_eq_one_iff_eq_inv, mul_eq_left, ←
            coe_one, ← Subtype.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(ofSubtype.noncommCoprod (noncommPiCoprod ⋯) ⋯)

Tactic:
MonoidHom.noncommCoprod_injective

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑ofSubtype ∧
    Function.Injective ⇑(noncommPiCoprod ⋯) ∧ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range
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
⊢ ∃ H, N.IsComplement' H

Tactic:
have h7 : Nat.card N * Nat.card (H.map K.subtype) = Nat.card G := by
    rw [hH, ← N.index_mul_card, mul_comm]

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
⊢ ∃ H, N.IsComplement' H
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card α)! = Fintype.card (ConjAct (Perm α))

Tactic:
rw [ConjAct.card, Fintype.card_perm]

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

Goal state before:
pp: case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
convert! Monoid.order_dvd_exponent (a 1)

Goal state after:
case e'_3
n : ℕ
hn : NeZero n
⊢ 2 * n = orderOf (a 1)
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
this : IsCyclic ↥(commutator ↥H)
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
let f := Subgroup.equivMapOfInjective (commutator H) _ H.subtype_injective

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
this : IsCyclic ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥(Subgroup.map H.subtype (commutator ↥H)) := (commutator ↥H).equivMapOfInjective H.subtype ⋯
⊢ IsCyclic ↥⁅H, H⁆
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
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h :
  Subgroup.map (Subgroup.normalizer ↑↑P).subtype ((↑P).subgroupOf (Subgroup.normalizer ↑↑P)) ≤
    Subgroup.map (Subgroup.normalizer ↑↑P).subtype (commutator ↥(Subgroup.normalizer ↑↑P))
⊢ ↑P ≤ commutator G

Tactic:
Subgroup.map_subgroupOf_eq_of_le P.le_normalizer,

Goal state after:
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
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑P ≤ Subgroup.map (Subgroup.normalizer ↑↑P).subtype (commutator ↥(Subgroup.normalizer ↑↑P))
⊢ ↑P ≤ commutator G
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

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

Tactic:
refine ⟨fun p hp P ↦ ?_⟩
  have := Fact.mk hp
  replace h_cop := (h_cop.of_dvd ((Subgroup.card_dvd_of_le h_le).trans
    (Subgroup.card_range_dvd f)) (Subgroup.index_ker f' ▸ f'.range.card_subgroup_dvd_card))
  rcases P.2.le_or_disjoint_of_coprime h_cop with h | h
  · replace h_le : P ≤ f.range := h.trans h_le
    suffices IsCyclic (P.subgroupOf f.range) by
      have key := Subgroup.subgroupOfEquivOfLe h_le
      exact isCyclic_of_surjective key key.surjective
    obtain ⟨Q, hQ⟩ := Sylow.mapSurjective_surjective f.rangeRestrict_surjective p (P.subtype h_le)
    rw [Sylow.ext_iff, Sylow.coe_mapSurjective, Sylow.coe_subtype] at hQ
    exact hQ ▸ isCyclic_of_surjective _ (f.rangeRestrict.subgroupMap_surjective Q)
  · have := (P.2.map f').isCyclic_of_isZGroup
    apply isCyclic_of_injective (f'.subgroupMap P)
    rwa [← MonoidHom.ker_eq_bot_iff, P.ker_subgroupMap f', Subgroup.subgroupOf_eq_bot]

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

Goal state before:
pp: case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a ↦ (κ a) (if a ∈ t₁ then t₂ else ∅)

Tactic:
have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 := by
      ext1 a
      split_ifs
      exacts [rfl, measure_empty]

Goal state after:
case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite : (fun a ↦ (κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a ↦ if a ∈ t₁ then (κ a) t₂ else 0
⊢ Measurable fun a ↦ (κ a) (if a ∈ t₁ then t₂ else ∅)
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 : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((κ b.1).prod (η b.2)) s

Tactic:
Measure.prod_apply hs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (x : β), (η b.2) (Prod.mk x ⁻¹' s) ∂κ b.1
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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
x : α × γ
⊢ (κ ∥ₖ η) x = (κ x.1).prod (η x.2)

Tactic:
by
  rw [parallelComp, dif_pos ⟨inferInstance, inferInstance⟩, coe_mk]

Goal state after:
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.1).prod (η x.2)) s = ∫⁻ (b : β), (η x.2) (Prod.mk b ⁻¹' s) ∂κ x.1

Tactic:
Measure.prod_apply hs

Goal state after:
α : 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_1 : β), (η x.2) (Prod.mk x_1 ⁻¹' s) ∂κ x.1 = ∫⁻ (b : β), (η x.2) (Prod.mk b ⁻¹' s) ∂κ x.1
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 γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ a).prod (η a)) s = ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a

Tactic:
Measure.prod_apply hs

Goal state after:
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 γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a = ((κ a).prod (η a)) s

Tactic:
Measure.prod_apply hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a = ∫⁻ (x : β), (η a) (Prod.mk x ⁻¹' s) ∂κ a
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 γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
⊢ (κ ×ₖ η) a = (κ a).prod (η a)

Tactic:
ext s hs
  rw [prod_apply' _ _ _ hs, Measure.prod_apply hs]

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

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ Measurable fun y ↦ ((swap γ β) (x, y)) s

Tactic:
· simpa [swap_apply' _ hs, Prod.swap_prod_mk] using!
        measurable_const.indicator (measurable_prodMk_right hs)

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

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✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (κ ×ₖ η)

Tactic:
Kernel.prod

Goal state after:
α : 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✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (κ ∥ₖ η ∘ₖ copy α)
Module: Mathlib.Probability.Kernel.Composition.Prod

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✝¹ : IsFiniteKernel κ
η : Kernel α γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ ×ₖ η)

Tactic:
Kernel.prod

Goal state after:
α : 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✝¹ : IsFiniteKernel κ
η : Kernel α γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ ∥ₖ η ∘ₖ copy α)
Module: Mathlib.Probability.Kernel.Composition.Prod

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 α β
η : Kernel α γ
⊢ IsSFiniteKernel (κ ×ₖ η)

Tactic:
Kernel.prod

Goal state after:
α : 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 α β
η : Kernel α γ
⊢ IsSFiniteKernel (κ ∥ₖ η ∘ₖ copy α)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
⊢ ∀ᵐ (x : α) ∂ξ, κ x ⟂ₘ η x

Tactic:
have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0
⊢ ∀ᵐ (x : α) ∂ξ, κ x ⟂ₘ η x
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 : α
⊢ ∫⁻ (b : β), (η (x, b)) {x | b ∈ s} ∂κ x = (κ x) s

Tactic:
have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b := by
    intro b
    by_cases hb : b ∈ s <;> simp [hb]

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 : α
this : ∀ (b : β), (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b
⊢ ∫⁻ (b : β), (η (x, b)) {x | b ∈ s} ∂κ x = (κ x) s
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.1).prod ((ξ ∘ₖ η) a.2)) s

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
ξ : Measure α
hξ : SFinite ξ
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
⊢ ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
exact h.mono_ac ((hξμ.withDensity_rnDeriv hξν).compProd_left _)
      ((hξμ.withDensity_rnDeriv hξν).compProd_left _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
| (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)

Tactic:
Measure.haveLebesgueDecomposition_add μ ν

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
| ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂(η.restrict ht) (a, b) ∂(κ.restrict hs) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
Kernel.restrict_apply

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

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
⊢ (μ.tilted fun x ↦ c) = (μ Set.univ)⁻¹ • μ

Tactic:
simp only [Measure.tilted, withDensity_const, integral_const, smul_eq_mul]
    by_cases h_univ : μ Set.univ = ∞
    · simp only [measureReal_def, h_univ, ENNReal.toReal_top, zero_mul, div_zero,
      ENNReal.ofReal_zero, zero_smul, ENNReal.inv_top]
    congr
    rw [div_eq_mul_inv, mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀ (exp_pos _).ne', mul_one,
      measureReal_def, ← ENNReal.toReal_inv, ENNReal.ofReal_toReal]
    simp [h0.out]

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

Goal state before:
pp: case pos.h_add
α : 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
f g : β × γ → E
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
⊢ Integrable g ((κ ⊗ₖ η) a) →
    ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a →
      ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a →
        ∫ (z : β × γ), (f + g) z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a

Tactic:
i_g

Goal state after:
case pos.h_add
α : 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
f g : β × γ → E
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
i_g : Integrable g ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a →
    ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a →
      ∫ (z : β × γ), (f + g) z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a