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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
⊢ ∃ a, (mulActionHom_of_embedding G α n) a = ⟨s, hs⟩

Tactic:
obtain ⟨f : Fin n ↪ α, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ ∃ a, (mulActionHom_of_embedding G α n) a = ⟨s, hs⟩
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le, top_le_iff, normalizer_eq_top_iff] at hN

Goal state after:
case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : H.Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
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✝ c✝ : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 * mk b.1 b.2 ≤ mk a.1 a.2 * mk c.1 c.2
⊢ mk b.1 b.2 ≤ mk c.1 c.2

Tactic:
simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ a.1] at hab ⊢

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑a.2 * a.1 * (↑c.2 * b.1) ≤ ↑a.2 * a.1 * (↑b.2 * c.1)
⊢ ↑c.2 * b.1 ≤ ↑b.2 * c.1
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case unit
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
u : M
hu : IsUnit u
hm : Irreducible (f u)
⊢ ∃ u_1 m', IsUnit (f u_1) ∧ Irreducible m' ∧ u = u_1 * m'

Tactic:
| unit u hu =>

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g✝ : G
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (ofGroup g✝) then unitsSMulWithCancel φ u (ofGroup g✝) h
      else
        let g' := unitsSMulGroup φ d u (ofGroup g✝).head;
        cons (↑g'.1) u ((↑g'.2 * (ofGroup g✝).head⁻¹) • ofGroup g✝) ⋯ ⋯)
hcan2 : Cancels u (ofGroup g✝)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head).1) (-u)
      ((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head).2 *
          (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (ofGroup g✝) hcan2)
      ⋯ ⋯ =
    ofGroup g✝

Tactic:
simp [Cancels] at hcan2

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a
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)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
rw [sup_le_iff]
    constructor
    · rintro - ⟨a, rfl⟩
      exact ⟨(a, 1), by rw [noncommCoprod_apply, map_one, mul_one]⟩
    · rintro - ⟨a, rfl⟩
      exact ⟨(1, a), by rw [noncommCoprod_apply, map_one, one_mul]⟩

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

Goal state before:
pp: case refine_3
α : 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
⊢ y ∈ {x | Equiv.swap x y ∈ closure S}

Tactic:
rw [mem_ofPred, Equiv.swap_self]; apply one_mem

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ u ∈ (List.map Prod.fst w₂.toList).head?

Tactic:
← hw₂'2,

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ u ∈ (List.map Prod.fst w₁'.toList).head?
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1

Tactic:
rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup]
  exact forall_congr' fun g ↦ ⟨fun h hg ↦ h fun H ↦ hg H,
    fun h hg ↦ h fun H hH ↦ H.normalCore_le (hg (.ofSubgroup H.normalCore))⟩

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
⊢ ∀ (g : G), g ≠ 1 → ∃ H, H.FiniteIndex ∧ g ∉ H

Tactic:
intro g hg

Goal state after:
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
g : G
hg : g ≠ 1
⊢ ∃ H, H.FiniteIndex ∧ g ∉ H
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : ResiduallyFinite G
H : Subgroup G
⊢ ∀ (g : ↥H), (∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1) → g = 1

Tactic:
intro g hg

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : ResiduallyFinite G
H : Subgroup G
g : ↥H
hg : ∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1
⊢ g = 1
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : ResiduallyFinite G
inst✝ : ResiduallyFinite G'
⊢ ∀ (g : G × G'), (∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H) → g = 1

Tactic:
intro g hg

Goal state after:
G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : ResiduallyFinite G
inst✝ : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g = 1
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)
⊢ ∀ (x : Perm α), x ∉ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m}

Tactic:
intro g hg

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g ∈ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m}
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
refine ⟨ofSubtype_injective, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(noncommPiCoprod ⋯)

case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
⊢ 4 = 2

Tactic:
contrapose! hg0

Goal state after:
case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
hg0 : 4 ≠ 2
⊢ (-1) ^ (g.cycleType.sum + g.cycleType.card) ≠ 1
Module: Mathlib.GroupTheory.SchurZassenhaus

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

Tactic:
have := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3

Goal state after:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
this : IsMulCommutative ↥N
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ ((∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) →
    ∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α

Tactic:
rintro ⟨h_odd, h_fixed, h_count⟩ x hx
    rw [← kerParam_range_eq_centralizer_of_count_le_one h_count] at hx
    obtain ⟨⟨y, uv⟩, rfl⟩ := MonoidHom.mem_range.mp hx
    rw [mem_alternatingGroup, sign_kerParam_apply_apply (g := g) y uv]
    convert! mul_one _
    · apply Finset.prod_eq_one
      rintro ⟨c, hc⟩ _
      obtain ⟨k, hk⟩ := (uv _).prop
      rw [← hk, map_zpow]
      convert! one_zpow k
      rw [IsCycle.sign, Odd.neg_one_pow, neg_neg]
      · apply h_odd
        rw [cycleType_def, Multiset.mem_map]
        exact ⟨c, hc, rfl⟩
      · rw [mem_cycleFactorsFinset_iff] at hc
        exact hc.left
    · suffices y = 1 by simp [this]
      have := card_fixedPoints g
      exact card_support_le_one.mp <| le_trans (Finset.card_le_univ _) (by lia)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ {g | (↑g).IsThreeCycle} ⊆ ↑(⨆ s, (ofSubtype ↑s).range)

Tactic:
intro g hg

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : ↥(alternatingGroup α)
hg : g ∈ {g | (↑g).IsThreeCycle}
⊢ g ∈ ↑(⨆ s, (ofSubtype ↑s).range)
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:
by simpa using hα

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
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
⊢ kleinFour α ≤ commutator ↥(alternatingGroup α)

Tactic:
intro g hg

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : g ∈ kleinFour α
⊢ g ∈ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 4 = 1

Tactic:
by
  calc xa i ^ 4
      = a (n + n) := by simp [pow_succ, add_sub_assoc, sub_sub_cancel]
    _ = a ↑(2 * n) := by simp [Nat.cast_add, two_mul]
    _ = 1 := by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ {g | (↑g).cycleType = {2, 2}} ⊆ ↑(⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))

Tactic:
intro g hg

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : g ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ∈ ↑(⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))
Module: Mathlib.InformationTheory.Hamming

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

Tactic:
funext x y
  exact hammingDist_comm _ _

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind : (∀ i ∈ I, IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ insert i I, IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (∑ i ∈ insert i I, κs i)

Tactic:
rw [Finset.sum_insert hi_notMem_I]

Goal state after:
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind : (∀ i ∈ I, IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ insert i I, IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (κs i + ∑ x ∈ I, κs x)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
⊢ Measurable fun b ↦ (Measure.comap f (κ b)) t

Tactic:
have : (fun a => Measure.comap f (κ a) t) = fun a => κ a (f '' t) := by
      ext1 a
      rw [Measure.comap_apply _ hf.injective _ _ ht]
      exact fun s' hs' ↦ hf.measurableSet_image.mpr hs'

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this : (fun a ↦ (Measure.comap f (κ a)) t) = fun a ↦ (κ a) (f '' t)
⊢ Measurable fun b ↦ (Measure.comap f (κ b)) t
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
h' : sᶜ = ∅
⊢ μ = 0

Tactic:
simpa [μs, h'] using! measure_univ_le_add_compl s (μ := μ)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a ↦ ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂κ a

Tactic:
by
  unfold Function.const
  simp_rw [lintegral_indicator_const_comp measurable_prodMk_left ht _]
  exact Measurable.const_mul (measurable_kernel_prodMk_left ht) c

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 δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
⊢ deterministic f hf ∥ₖ deterministic g hg = deterministic (Prod.map f g) ⋯

Tactic:
ext x : 1
  simp_rw [parallelComp_apply, deterministic_apply, Prod.map, Measure.dirac_prod_dirac]

Goal state after:
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
⊢ IsFiniteKernel κ

Tactic:
by
  refine ⟨(fst κ).bound, (fst κ).bound_lt_top,
    fun a ↦ le_trans ?_ (measure_le_bound (fst κ) a Set.univ)⟩
  rw [fst_apply' _ _ MeasurableSet.univ]
  simp

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 γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
this : ∀ b ∈ t, (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 1
⊢ (κ x) {b | (b, f (x, b)) ∈ s} = ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x

Tactic:
rw [setLIntegral_congr_fun ht this, setLIntegral_one]

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
Y' : Type u_6
Z' : Type u_7
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')

Tactic:
rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp,
    ← parallelComp_comp_copy]

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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ ⊗ₖ η.restrict ht = (κ ⊗ₖ η).restrict ⋯

Tactic:
rw [← compProd_restrict MeasurableSet.univ ht]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ ⊗ₖ η.restrict ht = κ.restrict ⋯ ⊗ₖ η.restrict ht
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ κ ∘ₖ boolKernel μ ν = boolKernel (⇑κ ∘ₘ μ) (⇑κ ∘ₘ ν)

Tactic:
ext b : 1
  rw [comp_apply]
  cases b <;> simp

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

Goal state before:
pp: case pos
α : 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)
x : α
hfx : Integrable f (κ x)
⊢ Tendsto (fun i ↦ SimpleFunc.integral (κ x) (s i)) atTop (𝓝 (∫ (y : β), f y ∂κ x))

Tactic:
apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx

Goal state after:
case pos
α : 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 := ⋯
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := ⋯
f' : ℕ → α → E := ⋯
x : α
hfx : Integrable f (κ x)
⊢ range f ∪ {0} ⊆ range f ∪ {0}
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ (eLpNorm (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ).toReal ≤ ‖f‖

Tactic:
Lp.norm_def

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ (eLpNorm (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ).toReal ≤ (eLpNorm (↑↑f) 2 μ).toReal
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : G
⊢ ↑↑((condExpInd G hm μ s) c) =ᵐ[μ] ↑↑(indicatorConstLp 1 ⋯ hμs c)

Tactic:
indicatorConstLp_coeFn,

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : G
⊢ ↑↑((condExpInd G hm μ s) c) =ᵐ[μ] s.indicator fun x ↦ c
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
have h : ¬SigmaFinite (μ.trim bot_le) := by rwa [sigmaFinite_trim_bot_iff]
    rw [not_isFiniteMeasure_iff] at hμ_finite
    rw [condExp_of_not_sigmaFinite bot_le h]
    simp only [hμ_finite, ENNReal.toReal_top, inv_zero, zero_smul, measureReal_def]
    rfl

Goal state after: