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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ stabilizer (Perm α) sᶜ < G

Tactic:
stabilizer_compl

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ stabilizer (Perm α) s < G
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
⊢ False

Tactic:
apply hB'

Goal state after:
case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
⊢ Nat.card α < sᶜ.ncard * 2
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₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g ↦ S.inl n * s₂ g * (S.inl n)⁻¹
⊢ ⇑s₂ = fun g ↦ S.inl n⁻¹ * s₁ g * (S.inl n⁻¹)⁻¹

Tactic:
simp only [hn, map_inv]; group

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₂ s₃ : S.Splitting
h₁ : S.IsConj s₁ s₂
h₂ : S.IsConj s₂ s₃
⊢ S.IsConj s₁ s₃

Tactic:
obtain ⟨n₁, hn₁⟩ := h₁
  obtain ⟨n₂, hn₂⟩ := h₂
  exact ⟨n₁ * n₂, by simp only [hn₁, hn₂, map_mul]; group⟩

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
hf : Function.Surjective ⇑f
⊢ IsPerfect G'

Tactic:
by
  rw [← top_iff, ← MonoidHom.range_eq_top_of_surjective f hf]
  exact IsPerfect.range f

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)

Tactic:
intro hw x hx

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
hw : w.head ∈ toSubgroup A B u
x : G
hx : w.toList.head? = some (-u, x)
⊢ False
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_3
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : f y = x
z : N
hz : g z = x
⊢ x ∈ ⊥

Tactic:
rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy

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

Goal state before:
pp: case h.refine_2
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
⊢ Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod (f (m, s).1)

Tactic:
exact .trans (.trans (associated_unit_mul_right _ _ <|
        IsUnit.multisetProd_iff.mpr fun x hx ↦ (Multiset.mem_filter.mp hx).2) <| .of_eq <|
        (Multiset.prod_filter_mul_prod_filter_not _).trans (f.toMonoidHom.map_multiset_prod _).symm)
        ((factors_prod (mt (by simp [·]) hn)).map f)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right
α : 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
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
⊢ ∀ ⦃y : List ℕ⦄ (hy : ∀ a ∈ y, a < Fintype.card α), u.Disjoint y → (klift' u hu).Disjoint (klift' y hy)

Tactic:
v

Goal state after:
case h.right.right
α : 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
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
⊢ ∀ (hy : ∀ a ∈ v, a < Fintype.card α), u.Disjoint v → (klift' u hu).Disjoint (klift' v hy)
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 (σ * τ), ⋯⟩ = ⟨a.ofPermHom σ, ⋯⟩ * ⟨a.ofPermHom τ, ⋯⟩

Tactic:
simp only [map_mul, MulMemClass.mk_mul_mk]

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
⊢ m₁.left q = m₂.left q

Tactic:
have hh := fun a => (h a (m₁.right⁻¹ * q)).1
      rw [← (h a b).2] at hh
      group at hh
      exact FaithfulSMul.eq_of_smul_eq_smul hh

Goal state after:
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ᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ (unop g)⁻¹ * unop g = 1

Tactic:
inv_mul_cancel

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ 1 = 1
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 α)
⊢ ↑↑S = {1} ∪ {g | (↑g).cycleType = {2, 2}}

Tactic:
exact coe_two_sylow_of_card_eq_four hα4 S

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ 5 ≤ Nat.card α

Tactic:
simpa using hα

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (ZMod (2 * n) ⊕ ZMod (2 * n)) = 4 * n

Tactic:
Fintype.card_sum,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (ZMod (2 * n)) + Fintype.card (ZMod (2 * n)) = 4 * n
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
f : Perm α
hf : f.IsThreeCycle
⊢ normalClosure {⟨f, ⋯⟩} = ⊤

Tactic:
by
  have : IsSimpleGroup (alternatingGroup α) := isSimpleGroup h5
  apply normalClosure_normal.eq_bot_or_eq_top.resolve_left
  simp [hf.ne_one]

Goal state after:
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 : ι
⊢ ∀ {m₁ m₂ : G i}, (∀ (a : NormalWord d), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simp [summand_smul_def']

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

Goal state before:
pp: α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
⊢ Function.Injective fun L ↦ (↑L).flatten

Tactic:
intro L₁

Goal state after:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ : { L // ∀ (x : List α), x ∈ L → x ∈ S }
⊢ ∀ ⦃a₂ : { L // ∀ (x : List α), x ∈ L → x ∈ S }⦄, (fun L ↦ (↑L).flatten) L₁ = (fun L ↦ (↑L).flatten) a₂ → L₁ = a₂
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h : ⁅⊤, ⊤⁆ ≤ Subgroup.map ⊤.subtype ((Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆).subgroupOf ⊤)
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
Subgroup.map_subgroupOf_eq_of_le le_top

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h : ⁅⊤, ⊤⁆ ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h : ϕ k = ↑(n + 1)
⊢ k • g * g⁻¹ = g ^ n

Tactic:
rw [MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply rfl k g (n + 1) h,
      zpow_add_one, mul_inv_cancel_right]

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)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ⁅K, P⁆ = ⊥

Tactic:
eq_bot_iff,

Goal state after:
case refine_1
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ⁅K, P⁆ ≤ ⊥
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
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h :
  Subgroup.normalizer ↑P ≤
    Subgroup.centralizer ↑(Subgroup.map (Subgroup.normalizer ↑P).subtype ((↑P).subgroupOf (Subgroup.normalizer ↑P)))
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

Tactic:
← P.coe_coe,

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
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h :
  Subgroup.normalizer ↑↑P ≤
    Subgroup.centralizer ↑(Subgroup.map (Subgroup.normalizer ↑↑P).subtype ((↑P).subgroupOf (Subgroup.normalizer ↑↑P)))
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
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:
← P.coe_coe,

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 :
  Subgroup.map (Subgroup.normalizer ↑↑P).subtype ((↑P).subgroupOf (Subgroup.normalizer ↑↑P)) ≤
    Subgroup.map (Subgroup.normalizer ↑↑P).subtype (commutator ↥(Subgroup.normalizer ↑↑P))
⊢ ↑P ≤ commutator G
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 : t ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)

Tactic:
| basic t ht =>

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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
x : α × γ
⊢ (if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then { toFun := fun x ↦ (κ x.1).prod (η x.2), measurable' := ⋯ } else 0)
      x =
    (κ x.1).prod (η x.2)

Tactic:
dif_pos ⟨inferInstance, inferInstance⟩,

Goal state after:
α : 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 : α × γ
⊢ { toFun := fun x ↦ (κ x.1).prod (η x.2), measurable' := ⋯ } x = (κ x.1).prod (η x.2)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).map f) a) s = ∑' (i : ℕ), ((κ.seq i) a) (f ⁻¹' s)

Tactic:
simp_rw [map_apply' _ hf _ hs]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η b) (f ⁻¹' s) ∂κ a = ∫⁻ (b : β), ((η.map f) b) s ∂κ a

Tactic:
simp_rw [map_apply' _ hf _ hs]

Goal state after:
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
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ ((κ.map fun x ↦ (f x, g x)) x) (Prod.snd ⁻¹' s) = ((κ.map g) x) s

Tactic:
map_apply' _ (hf.prod hg),

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ (κ x) ((fun x ↦ (f x, g x)) ⁻¹' Prod.snd ⁻¹' s) = ((κ.map g) x) s

case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' 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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (a : Y × T), (Measure.dirac a.swap) s ∂(κ ac.1).prod (η ac.2) = ∫⁻ (b : T), (κ ac.1) (Prod.mk b ⁻¹' s) ∂η ac.2

Tactic:
rw [MeasureTheory.lintegral_prod_symm]

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 η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (y : T), ∫⁻ (x : Y), (Measure.dirac (x, y).swap) s ∂κ ac.1 ∂η ac.2 = ∫⁻ (b : T), (κ ac.1) (Prod.mk b ⁻¹' s) ∂η ac.2

case pos.hf
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 η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (Measure.dirac a.swap) s) ((κ ac.1).prod (η ac.2))
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
⊢ (⇑κ ∘ₘ μ) s = ∑' (i : α), (μ {i} • κ i) s

Tactic:
Measure.bind_apply hs (by fun_prop)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) s ∂μ = ∑' (i : α), (μ {i} • κ i) s
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
⊢ MeasurableSet t₁ →
    MeasurableSet t₂ →
      ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
intro ht₁ ht₂

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind.e_a.hfm
α : 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 (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ AEMeasurable (fun x ↦ (η (a, x)) (Prod.mk x ⁻¹' s)) (κ a)

Tactic:
exact (Kernel.measurable_kernel_prodMk_left' hs _).aemeasurable

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
· rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀]
    · simp only [Pi.mul_apply]
    · refine AEMeasurable.restrict ?_
      exact ((measurable_exp.comp_aemeasurable hf).div_const _).ennreal_ofReal
    · exact hs
    · filter_upwards
      simp only [ENNReal.ofReal_lt_top, implies_true]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
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 : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ Integrable f ((κ.restrict hs ⊗ₖ η.restrict ht) a)

Tactic:
compProd_restrict,

Goal state after:
α : 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ Integrable f (((κ ⊗ₖ η).restrict ⋯) a)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)).map ⇑MeasurableEquiv.prodAssoc.symm = κ ⊗ₖ η ⊗ₖ ξ

Tactic:
by
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [hκ]
  by_cases hη : IsSFiniteKernel η
  swap; · simp [hη]
  by_cases hξ : IsSFiniteKernel ξ
  swap
  · have : ¬ IsSFiniteKernel
        (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)) := by
      refine fun h_sfin ↦ hξ ?_
      have : ξ = (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)).comap
          MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _) := by
        simp [← comap_comp_right]
      rw [this]
      infer_instance
    simp [hξ, this]
  ext a s hs
  rw [compProd_apply hs, map_apply' _ (by fun_prop) _ hs,
    compProd_apply (hs.preimage (by fun_prop)), lintegral_compProd]
  swap; · exact measurable_kernel_prodMk_left' hs a
  congr with b
  rw [compProd_apply]
  · congr
  · exact hs.preimage (by fun_prop)

Goal state after: