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

Goal state before:
pp: case refine_1
α : 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
f : Equiv.Perm α
hf : f ∈ S
⊢ f⁻¹ ∈ S

pp: case refine_2
α : 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
z : α
hz : z ∈ {x | Equiv.swap x y ∈ closure S}
⊢ z ∈ orbit (↥(closure S)) x

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:
· obtain ⟨x, y, -, rfl⟩ := hS f hf; rwa [swap_inv]

Goal state after:
case refine_2
α : 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
z : α
hz : z ∈ {x | Equiv.swap x y ∈ closure S}
⊢ z ∈ orbit (↥(closure S)) x

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}
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case e_6.e_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := ⋯
⊢ c = ⟨g.cycleOf x, hx''⟩

Tactic:
← Subtype.coe_inj,

Goal state after:
case e_6.e_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
⊢ ↑c = ↑⟨g.cycleOf x, hx''⟩
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
⊢ (if b = a then a else if f b = a then f a else f b) = b

Tactic:
by_cases hb' : f b = b

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : f b = b
⊢ (if b = a then a else if f b = a then f a else f b) = b

case neg
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : ¬f b = b
⊢ (if b = a then a else if f b = a then f a else f b) = b
Module: Mathlib.GroupTheory.ResiduallyFinite

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

Tactic:
by
  simp_rw [residuallyFinite_def, Subgroup.eq_bot_iff_forall, Subgroup.mem_iInf,
    FiniteIndexNormalSubgroup.mem_toSubgroup_iff]

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
inst✝ : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op (g₂⁻¹ * g₁⁻¹) • α) T = (fun α ↦ op g₁⁻¹ • α) ((fun α ↦ op g₂⁻¹ • α) T)

Tactic:
exact mul_smul (op g₁⁻¹) (op g₂⁻¹) T

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 : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
x✝ : PushoutI φ →* K
⊢ ∀ (i : ι),
    ((fun f ↦ lift (↑f).1 (↑f).2 ⋯) ((fun f ↦ ⟨(fun i ↦ f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (of i) =
      x✝.comp (of i)

Tactic:
simp [DFunLike.ext_iff]

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 : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
x✝ : PushoutI φ →* K
⊢ ((fun f ↦ lift (↑f).1 (↑f).2 ⋯) ((fun f ↦ ⟨(fun i ↦ f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (base φ) =
    x✝.comp (base φ)

Tactic:
simp [DFunLike.ext_iff]

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⟩
⊢ #(↑(τ x)).support = #(↑x).support

Tactic:
rw [hx', Equiv.swap_apply_right]; 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 = ⊤

pp: case refine_2
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 ≠ ⊤

Tactic:
· have key : (N.map (QuotientGroup.mk' K)).comap (QuotientGroup.mk' K) = N := by
      refine comap_map_eq_self ?_
      rwa [QuotientGroup.ker_mk']
    rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]

Goal state after:
case refine_2
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 ≠ ⊤
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
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
P : Sylow (Nat.card ↥N).minFac ↥N
⊢ (↑P).subtype.range = ⊤

Tactic:
range_subtype

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
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
P : Sylow (Nat.card ↥N).minFac ↥N
⊢ ↑P = ⊤
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 = kleinFour α

Tactic:
kleinFour,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ↑S = Subgroup.closure {g | (↑g).cycleType = {2, 2}}
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ ∀ (a b c : QuaternionGroup n), a * b * c = a * (b * c)

Tactic:
unfold instHMul
    rintro (i | i) (j | j) (k | k) <;> simp only [mul] <;> ring_nf
    have : (2 * n : ZMod (2 * n)) = 0 := by norm_cast; simp
    grind

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
Q : Sylow p G
hG : IsCyclic ↥↑Q
⊢ IsCyclic ↥↑(Sylow.mapSurjective hf Q)

Tactic:
exact isCyclic_of_surjective _ (f.subgroupMap_surjective Q)

Goal state after:
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⁆
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
suffices h : commutator (commutator H) ≤ Subgroup.center (commutator H) by
      rw [← Abelianization.ker_of (commutator H)] at h
      let _ := commGroupOfCyclicCenterQuotient Abelianization.of h
      infer_instance

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⁆
⊢ commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥H)
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg.inl
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic 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 ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
hϕ : ∀ (a : K), ϕ a = 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
exact Or.inl fun p k ↦ by rw [h p k 0 (by rw [hϕ, sub_self, Int.cast_zero]), zpow_zero]

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

Tactic:
have hg₂r : g₂ ∉ (φ j).range := by
        rintro ⟨y, rfl⟩
        subst hg₂
        exact hx (of_apply_eq_base φ j y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)

Goal state after:
ι : 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
⊢ False
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
i : ι
a✝ : i ∈ univ
⊢ f i (x i) = f i (y i) → x i = y i

Tactic:
exact @hf _ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
g' : γ → ℝ≥0∞
hg : Measurable g'
⊢ ∫⁻ (b : γ), g' b ∂(κ.map f) a = ∫⁻ (a : β), g' (f a) ∂κ a

Tactic:
by
  rw [map_apply _ hf, lintegral_map hg hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ Kernel.const α ν) s = (μ.prod ν) s

Tactic:
simp_rw [compProd_apply hs, prod_apply hs, Kernel.const_apply]

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 γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ.snd a) s = (κ a) (Prod.snd ⁻¹' s)

Tactic:
snd_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (Measure.map Prod.snd (κ a)) s = (κ a) (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
· exact withDensity_absolutelyContinuous _ _

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), False
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Kernel.id = deterministic Prod.fst ⋯ ×ₖ deterministic Prod.snd ⋯

Tactic:
deterministic_prod_deterministic

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Kernel.id = deterministic (fun a ↦ (a.1, a.2)) ⋯
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:
by
  rw [← compProd_restrict MeasurableSet.univ ht]
  congr; exact Kernel.restrict_univ.symm

Goal state after:
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 := ⋯
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := ⋯
s' : ℕ → α → SimpleFunc β E := ⋯
f' : ℕ → α → E := ⋯
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) (κ x)
n : ℕ
⊢ ∀ᵐ (a : β) ∂κ x, ‖(s' n x) a‖ ≤ ((fun a ↦ ‖f x a‖) + fun a ↦ ‖f x a‖) a

Tactic:
filter_upwards with y

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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) (κ x)
n : ℕ
y : β
⊢ ‖(s' n x) y‖ ≤ ((fun a ↦ ‖f x a‖) + fun a ↦ ‖f x a‖) y
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int✝ :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top✝ : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_mul_eq : ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
h_int : Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
⊢ f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂η a).toReal =
    f (∫ (b : 𝓨), ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂η a)

Tactic:
by
    rw [integral_toReal (by fun_prop) h_lt_top]

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ ¬DifferentiableWithinAt ℝ klFun (Ioi 0) 0

Tactic:
by
  refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi _ ?_
  rw [deriv_klFun]
  exact tendsto_log_nhdsGT_zero

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ ¬DifferentiableWithinAt ℝ klFun (Iio 0) 0

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio _ ?_
  rw [deriv_klFun]
  exact tendsto_log_nhdsLT_zero

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)

Tactic:
limsup_eq

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ sInf {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : (μ.trim hm) s < ∞
⊢ IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)

Tactic:
trim_measurableSet_eq hm hs

Goal state after:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : (μ.trim hm) s < ∞
⊢ IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)

Tactic:
trim_measurableSet_eq hm hs

Goal state after:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)