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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ β✝ : H.QuotientDiff
β α : H.LeftTransversal
⊢ diff (MonoidHom.id ↥H) β α * (diff (MonoidHom.id ↥H) β α)⁻¹ = 1

Tactic:
mul_inv_cancel

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ β✝ : H.QuotientDiff
β α : H.LeftTransversal
⊢ 1 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ 1 < Fintype.card ↑(Function.fixedPoints ⇑g)

Tactic:
rwa [card_fixedPoints g, Nat.lt_iff_add_one_le, Nat.le_sub_iff_add_le]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ g.cycleType.sum ≤ Fintype.card α
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
⊢ (QuotientGroup.mk' K).ker ≤ N

Tactic:
by rwa [QuotientGroup.ker_mk']

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
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
H : ⟨c, hc⟩ ≠ ⟨d, hd⟩
⊢ ∑ x ∈ {⟨c, hc⟩, ⟨d, hd⟩}, #(↑x).support = #c.support * 2

Tactic:
Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),

Goal state after:
α : 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
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
H : ⟨c, hc⟩ ≠ ⟨d, hd⟩
⊢ #(↑⟨c, hc⟩).support + ∑ x ∈ {⟨d, hd⟩}, #(↑x).support = #c.support * 2
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg.inr
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)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
p : G
⊢ v.cast * u.cast ≡ 1 [ZMOD ↑(orderOf p)]

Tactic:
exact hvu.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard p))

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

Goal state before:
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
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑Q ≤ commutator ↥(Subgroup.normalizer ↑P)
⊢ ↑P ≤ commutator G

Tactic:
· rw [P.coe_subtype, ← Subgroup.map_subtype_le_map_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer, Subgroup.map_subtype_commutator] at h
    exact h.trans (Subgroup.commutator_mono le_top le_top)

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

Goal state before:
pp: case inr
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
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ f'.ker.subgroupOf ↑P = ⊥

Tactic:
Subgroup.subgroupOf_eq_bot

Goal state after:
case inr
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
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ Disjoint f'.ker ↑P
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ #{i | x i ≠ x i} = 0

Tactic:
card_eq_zero,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ {i | x i ≠ x i} = ∅
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ #{i | x i ≠ y i} = 0 → x = y

Tactic:
card_eq_zero,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ {i | x i ≠ y i} = ∅ → x = y
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)) = Measure.comap f (Measure.sum fun n ↦ (κ.seq n) a)

Tactic:
ext1 t ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
b : Bool
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((boolKernel μ ν) b) s✝ = ((Kernel.sum fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)) b) s✝

Tactic:
rw [Kernel.sum_apply]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
b : Bool
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((boolKernel μ ν) b) s✝ = (Measure.sum fun n ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)) b) s✝
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
⊢ deterministic f hf ∥ₖ deterministic g hg = deterministic (Prod.map f g) ⋯

Tactic:
ext x : 1

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
⊢ (deterministic f hf ∥ₖ deterministic g hg) x = (deterministic (Prod.map f g) ⋯) x
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ ⊗ₘ κ) (s ×ˢ t) = ∫⁻ (a : α) in s, (κ a) t ∂μ

Tactic:
by
  simp [compProd, Kernel.compProd_apply_prod hs ht]

Goal state after:
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:
simp_rw [← 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.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun x ↦ 1) (f b) ∂κ a = (κ a) (f ⁻¹' s)

Tactic:
lintegral_indicator_const_comp hf hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ 1 * (κ a) (f ⁻¹' s) = (κ a) (f ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
⊢ SFinite (μ ⊗ₘ κ)

Tactic:
by rw [compProd]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
s : Set (α × β)
hs : MeasurableSet s
⊢ ((Kernel.id ×ₖ κ) a) s = (κ a) (Prod.mk a ⁻¹' s)

Tactic:
by
  rw [Kernel.id, deterministic_prod_apply' _ _ _ hs, id_eq]

Goal state after:
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✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η

Tactic:
refine h _ ?_ ?_ ?_

Goal state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ SFinite (ν.withDensity (μ.rnDeriv ν))

case refine_2.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

case refine_2.refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν
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 α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Tactic:
by_cases hμ : IsSFiniteKernel μ
  swap; · simp [hμ]
  ext a s hs
  simp only [compProd_apply hs, FunLike.coe_add, Pi.add_apply, Measure.coe_add]
  rw [lintegral_add_left]
  exact measurable_kernel_prodMk_left' hs a

Goal state after:
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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ∞
⊢ (fun b ↦ ∫⁻ (c : γ), ‖f c‖ₑ ∂η b) =ᵐ[κ a] fun a ↦ ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal

Tactic:
filter_upwards [h] with x hx

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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ∞
x : β
hx : ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ∞
⊢ ∫⁻ (c : γ), ‖f c‖ₑ ∂η x = ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η x).toReal
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 α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ ∫ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a

Tactic:
refine integral_congr_ae ?_
  filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
  simp [integral_sub h2f h2g]

Goal state after:
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
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ Integrable f ((Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ) ()) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ

Tactic:
ProbabilityTheory.integrable_compProd_iff 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
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ (∀ᵐ (x : α) ∂(Kernel.const Unit μ) (), Integrable (fun y ↦ f (x, y)) ((prodMkLeft Unit κ) ((), x))) ∧
      Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂(prodMkLeft Unit κ) ((), x)) ((Kernel.const Unit μ) ()) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
⊢ ∃ f, f ≠ 0

Tactic:
have : Nontrivial (Lp ℝ p μ) := nontrivial_Lp_real_of_nontrivial_Lp E p μ

Goal state after:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
this : Nontrivial ↥(Lp ℝ p μ)
⊢ ∃ f, f ≠ 0
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg.h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ μ ≪ c • ν

pp: case neg.h_int
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ Integrable (llr μ (c • ν)) μ

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    ↑c * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)

Tactic:
· exact hμν.smul_right (by simpa)

Goal state after:
case neg.h_int
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ Integrable (llr μ (c • ν)) μ

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    ↑c * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : ¬MeasurableSet s
x : G
⊢ condExpIndL1 hm μ s x = 0

Tactic:
by
  simp only [condExpIndL1, hs, dif_neg, not_false_iff, false_and]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ.rnDeriv ν =ᵐ[ν] 1

Tactic:
filter_upwards [h] with x hx

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x
⊢ μ.rnDeriv ν x = 1 x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Tactic:
setIntegral_congr_ae (hm s hs)
      ((Lp.coeFn_add (hf_Lp.toLp f) (hg_Lp.toLp g)).mono fun x hx _ => hx)

Goal state after:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, (↑↑(MemLp.toLp f hf_Lp) + ↑↑(MemLp.toLp g hg_Lp)) x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : 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 α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∫ (a : α) in s, (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) a ∂μ = 0

Tactic:
refine integral_eq_zero_of_forall_integral_inner_eq_zero 𝕜 _ ?_ ?_

Goal state after:
case refine_1
α : 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 α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)

case refine_2
α : 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 α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∀ (c : E'), ∫ (x : α) in s, ⟪c, (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) x⟫ ∂μ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ Integrable μ[f | m] μ

Tactic:
rw [condExp_of_not_sigmaFinite hm hμm]; exact integrable_zero _ _ _

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
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ ¬SigmaFinite (μ.trim ⋯)

Tactic:
rwa [sigmaFinite_trim_bot_iff]

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

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : ¬μ ≪ ν ∨ ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
cases h_ac with
    | inl h => simp [h]
    | inr h => simp [h]

Goal state after: