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

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a})
⊢ IsMultiplyPreprimitive G α 2

Tactic:
rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),
        is_one_preprimitive_iff]

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a})
⊢ IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this✝ : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
this : k = ↑g
⊢ k ∈ G

Tactic:
rw [this]; exact SetLike.coe_mem g

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
h : g ⟨x, hx⟩ = g ⟨y, hy⟩
this : f x = f y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simpa [← Subtype.coe_inj, hf.injective.eq_iff] using! this

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
⊢ sᶜ = univ

Tactic:
apply hsc.eq_univ_of_card_lt

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
⊢ Nat.card α < sᶜ.ncard * 2
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
motive : NormalWord d → Sort u_4
ofGroup : (g : G) → motive (NormalWord.ofGroup g)
cons :
  (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') →
            motive w → motive (NormalWord.cons g u w h1 h2)
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
mem_set : ∀ (u : ℤˣ) (g_1 : G), (u, g_1) ∈ { head := g, toList := l, chain := chain }.toList → g_1 ∈ d.set u
⊢ motive { head := g, toList := l, chain := chain, mem_set := mem_set }

Tactic:
induction l generalizing g with

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

Goal state before:
pp: case h.right.left
α : 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
s : List α
⊢ s ∈ map (map ⇑(Fintype.equivFin α).symm) l → s.Nodup

Tactic:
mem_map

Goal state after:
case h.right.left
α : 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
s : List α
⊢ (∃ a ∈ l, map (⇑(Fintype.equivFin α).symm) a = s) → s.Nodup
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
⊢ Equiv.swap x y ∈ closure S

Tactic:
by_contra h

Goal state after:
α : 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
⊢ False
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
⊢ f x✝ = 1 x✝

Tactic:
by_contra h

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
h : ¬f x✝ = 1 x✝
⊢ False
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)
x : α
⊢ a.ofPermHomFun τ (a.ofPermHomFun τ⁻¹ x) = x

Tactic:
rw [← ofPermHomFun_mul, mul_inv_cancel, ofPermHomFun_one]

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: 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}, (∀ (a : Λ × Q), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simp only [smul_def, Prod.mk.injEq, mul_left_inj, Prod.forall]

Goal state after:
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},
    (∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right) → m₁ = m₂
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
rw [notMem_support.mp hx, eq_comm, ← notMem_support,
      ofPermHomFun_apply_mem_support_cycle_iff]
    exact hx

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
⊢ Nat.card G ^ Nat.card (Fin n) = p ^ n

Tactic:
Nat.card_fin,

Goal state after:
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
⊢ Nat.card G ^ n = p ^ n
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⨅ H, H.toSubgroup = ⊥ ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1

Tactic:
Subgroup.eq_bot_iff_forall,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ (∀ x ∈ ⨅ H, H.toSubgroup, x = 1) ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : ResiduallyFinite G
g h : G
hgh : g ≠ h
H : FiniteIndexNormalSubgroup G
hH : g⁻¹ * h ∉ H
⊢ ↑g ≠ ↑h

Tactic:
by simpa [QuotientGroup.eq]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : ↥g.cycleFactorsFinset
⊢ #(↑(τ x)).support = #(↑x).support

Tactic:
by_cases hx : x = ⟨c, hc⟩
    · rw [hx, Equiv.swap_apply_left]; exact hm.symm
    by_cases hx' : x = ⟨d, hd⟩
    · rw [hx', Equiv.swap_apply_right]; exact hm
    · rw [Equiv.swap_apply_of_ne_of_ne hx hx']

Goal state after:
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'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ N.index * Nat.card ↥(map (QuotientGroup.mk' K) N) ∣ N.index * Nat.card ↥N

Tactic:
index_mul_card,

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'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ N.index * Nat.card ↥(map (QuotientGroup.mk' K) N) ∣ Nat.card G
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ #{g | g.cycleType = m} = 0 ↔ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff,
    ← exists_with_cycleType_iff, not_exists]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ⨆ s, (ofSubtype ↑s).range = ⊤

Tactic:
rw [eq_top_iff, ← closure_isThreeCycles_eq_top, Subgroup.closure_le]
    intro g hg
    apply Subgroup.mem_iSup_of_mem ⟨(g : Perm α).support, hg.card_support⟩
    rw [mem_range_ofSubtype_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
⊢ IsZGroup G

Tactic:
by
  have : Finite G := Nat.finite_of_card_ne_zero hG.ne_zero
  refine ⟨fun p hp P ↦ ?_⟩
  have := Fact.mk hp
  obtain ⟨k, hk⟩ := P.2.exists_card_eq
  exact isCyclic_of_card_dvd_prime ((hk ▸ hG.pow_dvd_of_pow_dvd) P.card_subgroup_dvd_card)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Nonempty α
⊢ ¬IsMarkovKernel 0

Tactic:
by_contra h

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Nonempty α
h : IsMarkovKernel 0
⊢ False
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ Kernel.sum κs = Kernel.sum fun n ↦ (κs (e n).1).seq (e n).2

Tactic:
have hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (seq (κs n)) := by
    simp_rw [kernel_sum_seq]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
⊢ Kernel.sum κs = Kernel.sum fun n ↦ (κs (e n).1).seq (e n).2
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : a ∈ s
⊢ κ a = Measure.sum fun n ↦ (κ.seq n) a

Tactic:
exact (measure_sum_seq _ a).symm

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : a ∉ s
⊢ η a = Measure.sum fun n ↦ (η.seq n) a

Tactic:
exact (measure_sum_seq _ a).symm

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 γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) a✝¹) s✝ = ((const α μ) a✝¹) s✝

Tactic:
simp_rw [const_comp, measure_univ, one_smul, const_apply]

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

Tactic:
refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a : α
⊢ ((η ∘ₖ κ) a) Set.univ ≤ κ.bound * η.bound
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (fun r ↦ ↑r * ↑maxLen / K ^ r) atTop (nhds 0)
⊢ ∃ r ≥ 1, ↑r * ↑(S.sup List.length) < (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r

Tactic:
obtain ⟨r, hr⟩ := eventually_atTop.mp <| this.eventually <| gt_mem_nhds zero_lt_one

Goal state after:
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (fun r ↦ ↑r * ↑maxLen / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ (b : ℕ), r ≤ b → ↑b * ↑maxLen / K ^ b < 1
⊢ ∃ r ≥ 1, ↑r * ↑(S.sup List.length) < (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = (κ a ⊗ₘ η.sectR a) s

Tactic:
simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]

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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ ∥ₖ η)

Tactic:
refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩

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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ ((κ ∥ₖ η) a) Set.univ ≤ κ.bound * η.bound
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = 0

Tactic:
← Kernel.compProd_zero_right κ

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = κ ⊗ₖ 0
Module: Mathlib.Probability.Kernel.MeasurableIntegral

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

Tactic:
refine StronglyMeasurable.indicator ?_ (measurableSet_kernel_integrable hf)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable (f x) (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s' n x)
n : ℕ
⊢ StronglyMeasurable fun x ↦ SimpleFunc.integral (κ x) (s' n x)
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
⊢ f (μ.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
have hf_cont' : ContinuousOn f (Ici 0) := hf_cvx.continuousOn_Ici hf_cont
  calc f (μ.real univ)
    = f (∫ x, (μ.rnDeriv ν x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν]
  _ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := by
    rw [← average_eq_integral, ← average_eq_integral]
    exact ConvexOn.map_average_le hf_cvx hf_cont' isClosed_Ici (by simp)
      Measure.integrable_toReal_rnDeriv hf_int

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a ∂μ = ∫⁻ (a : 𝓧) in s, (κ a) univ ∂μ

Tactic:
rw [← Measure.setLIntegral_compProd (by fun_prop) hs .univ, Measure.setLIntegral_rnDeriv hκη,
      Measure.compProd_apply_prod hs .univ]

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

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ μ ≪ μ.tilted f

Tactic:
refine withDensity_absolutelyContinuous' ?_ ?_

Goal state after:
case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ AEMeasurable (fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
rw [Measure.compProd, ProbabilityTheory.setIntegral_compProd hs ht hf]

Goal state after:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂(prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ