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

Goal state before:
pp: case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
Nat.card_eq_one_iff_unique

Goal state after:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Subsingleton ↥N ∧ Nonempty ↥N
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H
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
⊢ Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) * Nat.card ↥(kleinFour α) = 3 * Nat.card ↥(kleinFour α)

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card ↥(kleinFour α) ≠ 0

Tactic:
· rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]
      rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card ↥(kleinFour α) ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

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

Tactic:
ZMod.card,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ 2 * n + 2 * n = 4 * n
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case zero
n : ℕ
⊢ a 1 ^ 0 = a ↑0

Tactic:
Nat.cast_zero

Goal state after:
case zero
n : ℕ
⊢ a 1 ^ 0 = a 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: ⊢ IsCyclic (QuaternionGroup 1)

Tactic:
apply isCyclic_of_orderOf_eq_card
  · rw [Nat.card_eq_fintype_card, card, mul_one]
    exact orderOf_xa 0

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

Goal state before:
pp: case inl
n : ℕ
⊢ 0 < n → QuaternionGroup.a 1 ^ n ≠ 1

Tactic:
h

Goal state after:
case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ 1
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
⊢ H ≠ ⊥ → ⁅H, H⁆ < H

Tactic:
h

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
⊢ ⁅H, H⁆ < H
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
hG : Group.IsNilpotent G
⊢ IsCyclic G

Tactic:
have (p : { x // x ∈ (Nat.card G).primeFactors }) : Fact p.1.Prime :=
    ⟨Nat.prime_of_mem_primeFactors p.2⟩

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime ↑p)
⊢ IsCyclic G
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hα' : Nat.card α = 6
⊢ N = ⊥ ∨ N = ⊤

pp: case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hα' : ¬Nat.card α = 6
⊢ N = ⊥ ∨ N = ⊤

Tactic:
· apply normal_subgroup_eq_bot_or_eq_top_of_card_ne_eight hα (by grind)

Goal state after:
case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hα' : ¬Nat.card α = 6
⊢ N = ⊥ ∨ N = ⊤
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 : ι
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i ↦ Classical.decEq (G i)
a₁✝ a₂✝ : G i
⊢ ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(of i)) a₁✝ = ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(of i)) a₂✝ → a₁✝ = a₂✝

Tactic:
h

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 : ι
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i ↦ Classical.decEq (G i)
a₁✝ a₂✝ : G i
h : ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(of i)) a₁✝ = ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(of i)) a₂✝
⊢ a₁✝ = a₂✝
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)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i ↦ Classical.decEq (G i)
a₁✝ a₂✝ : H
⊢ ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₁✝ = ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₂✝ → a₁✝ = a₂✝

Tactic:
h

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)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i ↦ Classical.decEq (G i)
a₁✝ a₂✝ : H
h : ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₁✝ = ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : Nat.card K = 1
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
Nat.card_eq_one_iff_unique

Goal state after:
case pos
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : Subsingleton K ∧ Nonempty K
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : (κ a) s = (η a) s
⊢ (κ a) s = (η a) s

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : (κ a) s = (η a) s
⊢ (η a) s = (η a) s
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : κ = η
a : α
f : β → ℝ≥0∞
x✝ : Measurable f
⊢ ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : κ = η
a : α
f : β → ℝ≥0∞
x✝ : Measurable f
⊢ ∫⁻ (b : β), f b ∂η a = ∫⁻ (b : β), f b ∂η a
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η : Kernel α β
inst✝ : Countable ι
κ : ι → Kernel α β
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (Measure.sum fun n ↦ (κ n) b) s

Tactic:
simp_rw [Measure.sum_apply _ hs]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η : Kernel α β
inst✝ : Countable ι
κ : ι → Kernel α β
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∑' (i : ι), ((κ i) b) s
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
a : α
⊢ Kernel.id a = Measure.dirac a

Tactic:
by
  rw [Kernel.id, deterministic_apply, id_def]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 ↔ ¬0 < hammingDist x y

Tactic:
not_lt,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 ↔ hammingDist x y ≤ 0
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

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

Tactic:
← measure_univ_eq_zero

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∀ᵐ (a : α) ∂μ, (κ a) univ = 0
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ (μ ⊗ₘ κ) (univ ×ˢ univ) = 0

Tactic:
h

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ 0 (univ ×ˢ univ) = 0
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound

pp: case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : ¬Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound

Tactic:
· rw [map_apply' κ hf a MeasurableSet.univ]
    exact measure_le_bound κ a _

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : ¬Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound
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 γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ Kernel.id.map (g ∘ f) = deterministic (g ∘ f) ⋯

Tactic:
id_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ deterministic (g ∘ f) ?m.60 = deterministic (g ∘ f) ⋯

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ Measurable (g ∘ f)
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((κ ∘ₖ deterministic g hg) a) s = ((κ.comap g hg) a) s

Tactic:
comap_apply' _ _ _ s,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((κ ∘ₖ deterministic g hg) a) s = (κ (g a)) s
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ ((κ ⊗ₖ η) a) (Set.univ ×ˢ Set.univ) = 0

Tactic:
h

Goal state after:
case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ (0 a) (Set.univ ×ˢ Set.univ) = 0
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : (fun a ↦ (κ a) (Prod.mk a ⁻¹' h.nullSet)) =ᵐ[μ] 0
hν_zero : (fun a ↦ (η a) (Prod.mk a ⁻¹' h.nullSetᶜ)) =ᵐ[ν] 0
x : α
hxμ : (κ x) (Prod.mk x ⁻¹' h.nullSet) = 0 x
hxν : (η x) (Prod.mk x ⁻¹' h.nullSetᶜ) = 0 x
⊢ κ x ⟂ₘ η x

Tactic:
exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prodMk_left hs, ⟨hxμ, hxν⟩⟩

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
s : Set α
hs : MeasurableSet s
⊢ (⇑(Kernel.boolKernel μ ν) ∘ₘ π) s = (π {true} • ν + π {false} • μ) s

Tactic:
rw [Measure.bind_apply hs (Kernel.aemeasurable _)]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : Bool), ((Kernel.boolKernel μ ν) a) s ∂π = (π {true} • ν + π {false} • μ) s
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (μ.tilted fun x ↦ c) = (μ Set.univ)⁻¹ • μ

Tactic:
h

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (Measure.tilted 0 fun x ↦ c) = (0 Set.univ)⁻¹ • 0
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ AEStronglyMeasurable f ((κ ∘ₖ Kernel.const Unit μ) ())

Tactic:
simpa [Kernel.comp_apply]

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
h

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂Measure.tilted 0 f = (∫ (x : α), rexp ((f + g) x) ∂0) / ∫ (x : α), rexp (f x) ∂0
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
hfν : Integrable (fun x ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), -f x + log (∫ (x : α), rexp (f x) ∂ν) + llr μ ν x ∂μ =
    -∫ (x : α), f x ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
by
        rw [← integral_neg, integral_add ?_ h_int]
        swap; · exact hfμ.neg.add (integrable_const _)
        rw [integral_add ?_ (integrable_const _)]
        swap; · exact hfμ.neg
        simp only [integral_const, probReal_univ, smul_eq_mul, one_mul]

Goal state after:
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 t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
x : G
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ ⋯ 1))) =ᵐ[μ]
    ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm ht hμt x)

Tactic:
rw [indicatorConstLp_disjoint_union hs ht hμs hμt hst (1 : ℝ)]

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
x : G
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x))
          ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1 + indicatorConstLp 2 ht hμt 1))) =ᵐ[μ]
    ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm ht hμt x)
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
⊢ ∀ᵐ (a : X) ∂μ, ∑' (n : ι), ‖f n a‖ₑ < ∞

Tactic:
have A (s : Set X) (hs : MeasurableSet s) (h's : μ s ≠ ∞) :
      ∀ᵐ x ∂μ, x ∈ s → ∑' n, ‖f n x‖ₑ < ∞ := by
    rw [← ae_restrict_iff' hs]
    apply ae_lt_top' (AEMeasurable.tsum (fun i ↦ (hf i).restrict.enorm))
    rw [lintegral_tsum (fun i ↦ (hf i).restrict.enorm)]
    apply ne_of_lt
    have : ∑' n, eLpNorm (f n) p (μ.restrict s) *
        (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal) < ∞ := by
      rw [ENNReal.tsum_mul_right]
      apply ENNReal.mul_lt_top ?_ ?_
      · apply lt_of_le_of_lt ?_ h'f.lt_top
        gcongr
        exact Measure.restrict_le_self
      · simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, ENNReal.toReal_one,
          ne_eq, one_ne_zero, not_false_eq_true, div_self, one_div]
        apply ENNReal.rpow_lt_top_of_nonneg _ h's
        simp only [sub_nonneg]
        apply inv_le_one_of_one_le₀
        rw [← ENNReal.ofReal_le_iff_le_toReal h'p.ne]
        simpa
    apply lt_of_le_of_lt ?_ this
    gcongr with i
    rw [← eLpNorm_one_eq_lintegral_enorm]
    exact eLpNorm_le_eLpNorm_mul_rpow_measure_univ hp (hf i).restrict

Goal state after:
case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
⊢ ∀ᵐ (a : X) ∂μ, ∑' (n : ι), ‖f n a‖ₑ < ∞
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 t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ∞
⊢ condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x

Tactic:
condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x,

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ∞
⊢ condExpIndL1 hm μ (s ∪ t) x = condExpIndL1Fin hm hs hμs x + condExpIndL1 hm μ t x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_3
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))) μ

Tactic:
have h_coe := T.coeFn_compLp (condExpL2 E' 𝕜 hm f : α →₂[μ] E')
    rw [← EventuallyEq] at h_coe
    refine AEStronglyMeasurable.congr ?_ h_coe.symm
    exact T.continuous.comp_aestronglyMeasurable (lpMeas.aestronglyMeasurable (condExpL2 E' 𝕜 hm f))

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∀ᵐ (p : 𝓧 × 𝓨) ∂ν ⊗ₘ η,
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
by
  filter_upwards [rnDeriv_compProd h_ac ν] with p hp
  simp_rw [hp, ENNReal.toReal_mul]
  by_cases h_zero1 : ((∂μ/∂ν) p.1).toReal = 0
  · simp [h_zero1]
  by_cases h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
  · simp [h_zero2]
  simp [log_mul h_zero1 h_zero2]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
f : α → E
⊢ (fun x ↦ 1⁻¹ • ∫ (x : α), f x ∂μ) = fun x ↦ ∫ (x : α), f x ∂μ

Tactic:
inv_one,

Goal state after:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
f : α → E
⊢ (fun x ↦ 1 • ∫ (x : α), f x ∂μ) = fun x ↦ ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hμm_not : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] = 0

Tactic:
by simp [condLExp, dif_pos hm, hμm_not]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : Ω
⊢ X a✝ = Y a✝ → a✝ ∈ s → X a✝ = Y a✝

Tactic:
h

Goal state after:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : Ω
h : X a✝ = Y a✝
⊢ a✝ ∈ s → X a✝ = Y a✝
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
⊢ ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a → μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a → μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a

Tactic:
h

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a
⊢ μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a → μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a