mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
⊢ Fintype.card α ≤ g.cycleType.sum + 1

Tactic:
by
  by_contra! hm
  replace hm : 2 + g.cycleType.sum ≤ Fintype.card α := by lia
  suffices 1 < Fintype.card (Function.fixedPoints g) by
    obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this
    suffices sign (kerParam g ⟨swap a b, 1⟩) ≠ 1 from
      this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))
    simp [sign_kerParam_apply_apply, hab]
  rwa [card_fixedPoints g, Nat.lt_iff_add_one_le, Nat.le_sub_iff_add_le]
  rw [sum_cycleType]
  exact Finset.card_le_univ _

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

Goal state before:
pp: case pos
α : 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
hx : ¬x = ⟨c, hc⟩
hx' : x = ⟨d, hd⟩
⊢ #(↑⟨c, hc⟩).support = #(↑⟨d, hd⟩).support

Tactic:
exact hm

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case refine_1
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
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤

Tactic:
have key : (N.map (QuotientGroup.mk' K)).comap (QuotientGroup.mk' K) = N := by
      refine comap_map_eq_self ?_
      rwa [QuotientGroup.ker_mk']

Goal state after:
case refine_1
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
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 0 <
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
rw [← nat_card_centralizer g]
    apply Nat.card_pos

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc✝ : c ∈ g.cycleFactorsFinset
hc : c.IsCycle ∧ ∀ a ∈ c.support, c a = g a
a✝ : ⟨c, hc✝⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc✝⟩ ^ x) k = ↑(uv ⟨c, hc✝⟩)
⊢ (↑⟨c, hc✝⟩).IsCycle

Tactic:
exact hc.left

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ (∃ x ∈ kleinFour ↥s, (ofSubtype s) x = (ofSubtype s) σ) ↔
    ↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2}

Tactic:
ofSubtype_inj,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ (∃ x ∈ kleinFour ↥s, x = σ) ↔ ↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2}
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⁅⊥, ⊥⁆

Tactic:
rw [Subgroup.commutator_bot_left]

Goal state after:
case ind.inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⊥
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
⊢ Injective ⇑(base φ)

Tactic:
rcases transversal_nonempty φ hφ with ⟨d⟩
  let _ := Classical.decEq ι
  let _ := fun i => Classical.decEq (G i)
  refine Function.Injective.of_comp
    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_
  intro _ _ h
  exact eq_of_smul_eq_smul (fun w : NormalWord d =>
    by simp_all [funext_iff, base_smul_eq_smul])

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

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

Tactic:
L₂

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

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
x : PushoutI φ
g₁ : G i
hg₁ : (of i) g₁ = x
g₂ : G j
hg₂ : (of j) g₂ = x
hx : ¬x ∈ (base φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := { toList := [⟨i, g₁⟩, ⟨j, g₂⁻¹⟩], ne_one := ⋯, chain_ne := ⋯ }
⊢ Reduced φ w

Tactic:
simp only [w, Reduced, List.mem_cons,
          forall_eq_or_imp, not_false_eq_true,
          hg₁r, hg₂r, List.mem_nil_iff, false_imp_iff, imp_true_iff, and_true,
          inv_mem_iff]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ⊥
⊢ ↑P ≤ Subgroup.center G

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
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ↑P ≤ commutator G

Tactic:
· replace h := sup_le (Subgroup.commutator_eq_bot_iff_le_centralizer.mp h) P.le_centralizer
    rwa [hK.sup_eq_top, top_le_iff, Subgroup.centralizer_eq_top_iff_subset] at h

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
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ↑P ≤ commutator G
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ : Hamming β
⊢ ↑(hammingDist (ofHamming fst✝) (ofHamming fst✝)) = 0

Tactic:
exact mod_cast hammingDist_self _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (Set.range f) = 1

Tactic:
exact hκ a

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

Goal state before:
pp: case left
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ r ≤ ∑ i, (↑(w i)).length

Tactic:
have : ∑ _, 1 ≤ ∑ i, (w i).val.length :=
      Finset.sum_le_sum (fun i _ => by grind)

Goal state after:
case left
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
this : ∑ x, 1 ≤ ∑ i, (↑(w i)).length
⊢ r ≤ ∑ i, (↑(w i)).length
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case calc.step
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := ⋯
T : Finset (List α) := ⋯
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc r (r * maxLen)
D : ℝ := ⋯
⊢ ∑ i ∈ Finset.Icc r (r * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑r * ↑maxLen

Tactic:
rcases r with (_ | _ | r) <;> rcases maxLen with (_ | _ | maxLen)
    <;> simp at * <;> norm_cast <;> simp

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ac.1).prod (η ac.2) = ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1

Tactic:
MeasureTheory.lintegral_prod _ hg.aemeasurable

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (x : β), ∫⁻ (y : δ), g (x, y) ∂η ac.2 ∂κ ac.1 = ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
by
  by_cases hκ : IsSFiniteKernel κ
  · simp_rw [Measure.compProd, Kernel.const_add, Kernel.compProd_add_left, _root_.add_apply]
  · simp [hκ]

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 α β
f : β → γ
g : β → δ
hf : Measurable f
⊢ (κ.map fun x ↦ (f x, g x)).snd = κ.map g

Tactic:
by
  by_cases hg : Measurable g
  · ext x s hs
    rw [snd_apply' _ _ hs, map_apply' _ (hf.prod hg), map_apply' _ hg _ hs]
    · simp only [Set.preimage, Set.mem_ofPred]
    · exact measurable_snd hs
  · have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hg; exact hg.snd
    simp [map_of_not_measurable _ hg, map_of_not_measurable _ this]

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

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

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (ν ⊗ₘ κ) s = 0
⊢ (μ ⊗ₘ κ) s = 0
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

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

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (μ ⊗ₘ η) s = 0
⊢ (μ ⊗ₘ κ) s = 0
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 : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ a).prod (η a) = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a

Tactic:
MeasureTheory.lintegral_prod _ hg.aemeasurable

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

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

Tactic:
rw [compProd_of_not_isSFiniteKernel _ _ hη]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ 0
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
⊢ ∫⁻ (a : α), (κ a) s ∂μ = ∑' (i : α), (μ {i} • κ i) s

Tactic:
simp [lintegral_countable', mul_comm]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ ((κ ⊗ₖ η) a) {a | ¬p a} = 0

Tactic:
compProd_null

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' {a | ¬p a})) =ᵐ[κ a] 0

case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ MeasurableSet {a | ¬p a}
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
⊢ ⇑κ ∘ₘ μ ≪ ⇑κ ∘ₘ ν

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Goal state after:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : (⇑κ ∘ₘ ν) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
⊢ ⇑κ ∘ₘ μ ≪ ⇑η ∘ₘ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (⇑η ∘ₘ μ) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0
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
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i ↦ ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)

Tactic:
have (i : Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))) :
      Measurable fun z => ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm

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
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᵐ[μ] g
⊢ μ.tilted f = μ.tilted g

Tactic:
by
  have h_int_eq : ∫ x, exp (f x) ∂μ = ∫ x, exp (g x) ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hfg] with x hx
    rw [hx]
  refine withDensity_congr_ae ?_
  filter_upwards [hfg] with x hx
  rw [h_int_eq, hx]

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

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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ (η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)) a) (⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) =
    ∫⁻ (b : β × γ), (ξ (a, b)) (Prod.mk b ⁻¹' s) ∂(κ ⊗ₖ η) a

Tactic:
compProd_apply (hs.preimage (by fun_prop)),

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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      ((η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯) (a, b)) (Prod.mk b ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂κ a =
    ∫⁻ (b : β × γ), (ξ (a, b)) (Prod.mk b ⁻¹' s) ∂(κ ⊗ₖ η) a
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ Integrable f (⇑κ ∘ₘ μ) ↔ (∀ᵐ (x : α) ∂μ, Integrable f (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f y‖ ∂κ x) μ

Tactic:
rw [Measure.comp_eq_comp_const_apply, ProbabilityTheory.integrable_comp_iff]
  · simp
  · simpa [Kernel.comp_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
⊢ ↑↑f =ᵐ[μ] ↑↑g

Tactic:
suffices h_sub : ⇑(f - g) =ᵐ[μ] 0 by
    rw [← sub_ae_eq_zero]; exact (Lp.coeFn_sub f g).symm.trans h_sub
  have hfg' : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
    exact sub_eq_zero.mpr (hfg s hs hμs)
  have hfg_int : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (⇑(f - g)) s μ := by
    intro s hs hμs
    rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]
    exact (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
  exact Lp.ae_eq_zero_of_forall_setIntegral_eq_zero' 𝕜 hm (f - g) hp_ne_zero hp_ne_top hfg_int hfg'
    <| (hf_meas.sub hg_meas).congr (Lp.coeFn_sub f g).symm

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s ≤ ∫ (x : α) in {x | g x ≤ 0} ∩ s, g x ∂μ

Tactic:
Measure.restrict_restrict h_meas_nonpos_f,

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | f x ≤ 0} ∩ s, f x ∂μ ≤ ∫ (x : α) in {x | g x ≤ 0} ∩ s, g x ∂μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := (ν univ)⁻¹ • ν
hμν' : μ ≪ ν'
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
have h := integral_llr_add_sub_measure_univ_nonneg hμν' ?_

Goal state after:
case neg.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := (ν univ)⁻¹ • ν
hμν' : μ ≪ ν'
h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

case neg.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := (ν univ)⁻¹ • ν
hμν' : μ ≪ ν'
⊢ Integrable (llr μ ν') μ