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

Goal state before:
pp: case e'_3
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card ↥(ofStabilizer G a)

Tactic:
{

Goal state after:
case e'_3
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card ↥(ofStabilizer G a)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ {x | x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ}.card = 2

Tactic:
← card_support_eq_two.mpr h2g

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ {x | x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ}.card = g.support.card
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
have := (f.map_units (s₁ * s₂)).dvd_mul_right.mpr dvd

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this : f m ∣ n₁ * n₂ * f ↑(s₁ * s₂)
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsSwap
⊢ (fixedBy α σ)ᶜ.Finite

Tactic:
obtain ⟨x, y, -, rfl⟩ := h
  exact finite_compl_fixedBy_swap

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

Tactic:
obtain ⟨x, y, -, rfl⟩ := hS f hf; rwa [swap_inv]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
⊢ ¬∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
push Not

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
⊢ ∀ (a : ↥g.cycleFactorsFinset), ↑τ a ≠ a → ↑a x = x
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
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ∏ q, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ∏ x, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ * h

Tactic:
refine Finset.prod_congr rfl fun q _ => ?_

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ * h
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a.left.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a * g = g * ofSubtype a

Tactic:
exact Disjoint.commute (disjoint_iff_disjoint_support.mpr (ofSubtype_support_disjoint a))

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_2
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
this :
  ↑(⟨(φ i) h, ⋯⟩ * (⋯.equiv ((Word.equivPair i) w).head).1, (⋯.equiv ((Word.equivPair i) w).head).2).2 =
    (φ i) h * ((Word.equivPair i) w).head
⊢ h = 1

Tactic:
hhead

Goal state after:
case refine_2
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
this : ((Word.equivPair i) w).head = (φ i) h * ((Word.equivPair i) w).head
⊢ h = 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case neg
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw✝ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : ¬w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
simp [head?_eq_some_head hw, Word.fstIdx, hep hw]

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

Goal state before:
pp: n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 4 = a (↑n + ↑n)

Tactic:
by simp [pow_succ, add_sub_assoc, sub_sub_cancel]

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
hG : IsZGroup G
hf : Function.Surjective ⇑f
⊢ IsZGroup G'

Tactic:
rw [isZGroup_iff] at hG ⊢
  intro p hp P
  have := Fact.mk hp
  obtain ⟨Q, rfl⟩ := Sylow.mapSurjective_surjective hf p P
  specialize hG p hp Q
  exact isCyclic_of_surjective _ (f.subgroupMap_surjective Q)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
⊢ κ.bound < ∞

Tactic:
obtain ⟨C, hC, hle⟩ := h.exists_univ_le
  refine lt_of_le_of_lt ?_ hC
  simp [bound, hle]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_ <;>
      refine fun hP h ↦ P.not_dvd_index (h.trans ?_)
  · rw [(MonoidHom.ker_transferSylow_isComplement' P hP).index_eq_card]
    exact Subgroup.card_dvd_of_le (Abelianization.commutator_subset_ker _)
  · exact Subgroup.index_dvd_of_le hP

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

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

Tactic:
exact h.elim a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
ht : MeasurableSet t
⊢ ((κ.restrict hs) a) t = (κ a) (t ∩ s)

Tactic:
restrict_apply κ hs a,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
ht : MeasurableSet t
⊢ ((κ a).restrict s) t = (κ a) (t ∩ s)
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image concatFn Finset.univ
w✝ : Fin r → ↥S
left✝ : w✝ ∈ Finset.univ
hx : concatFn w✝ ∈ T
c : ↥S
hnil : ↑c = []
⊢ [] ∈ ↑S

Tactic:
simpa [hnil] using c.prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
⊢ μ (toMeasurable μ {a | ¬IsProbabilityMeasure (κ a)}) = 0

Tactic:
simpa [measure_toMeasurable] using! h

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
x : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((Measure.sum fun n ↦ (κ n) x.1).prod (η x.2)) s✝ = (Measure.sum fun n ↦ ((κ n) x.1).prod (η x.2)) s✝

Tactic:
Measure.prod_sum_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ∫⁻ (a : β), (η (f a)) s ∂κ x = ∫⁻ (b : β), ((η.comap f hf) b) s ∂κ x

Tactic:
comap_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 γ
inst✝ : Nonempty γ
κ : Kernel α β
⊢ IsSFiniteKernel (prodMkRight γ κ) ↔ IsSFiniteKernel κ

Tactic:
inhabit γ
  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  rw [← sectL_prodMkRight γ κ default]
  infer_instance

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

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

Tactic:
simp_rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
| μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
μ.haveLebesgueDecomposition_add ν

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
| (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

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

Tactic:
by
  ext s hs
  rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
  simp [lintegral_fintype, mul_comm]

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

Goal state before:

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

Goal state after:
Module: Mathlib.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 : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.stronglyMeasurable_mk]

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 : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (AEStronglyMeasurable.mk f hf) (η x)) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖AEStronglyMeasurable.mk f hf y‖ ∂η x) (κ a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x) (κ a)
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ ¬(rexp (f x) = 0 ∨ ∫ (x : α), rexp (f x) ∂μ = 0)

Tactic:
push Not

Goal state after:
case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) ≠ 0 ∧ ∫ (x : α), rexp (f x) ∂μ ≠ 0
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ klFun 0 = 1

Tactic:
simp [klFun]

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

Goal state before:
pp: ⊢ klFun 1 = 0

Tactic:
simp [klFun]

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
⊢ klDiv μ (c • ν) = ↑c * klDiv (c⁻¹ • μ) ν

Tactic:
have hμν_right := hμν.smul_right hc'

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ ↑c • ν
⊢ klDiv μ (c • ν) = ↑c * klDiv (c⁻¹ • μ) ν
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) μ
h_sub : ↑↑(f - g) =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] ↑↑g

Tactic:
rw [← sub_ae_eq_zero]

Goal state after:
α : 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) μ
h_sub : ↑↑(f - g) =ᵐ[μ] 0
⊢ ↑↑f - ↑↑g =ᵐ[μ] 0
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : ↑c ≠ 0
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν

Tactic:
have hμ_smul (μ : Measure α) : μ = c⁻¹ • (c • μ) := by
    rw [smul_smul, inv_mul_cancel₀ hc, one_smul]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : ↑c ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: 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 μ ν') μ

Tactic:
integrable_congr (llr_smul_right hμν (ν univ)⁻¹ (by simp) (by simp [hν]))

Goal state after:
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 (fun x ↦ llr μ ν x - log (ν univ)⁻¹.toReal) μ
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
⊢ condExpIndL1Fin hm ⋯ ⋯ x = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x

Tactic:
ext1
  grw [Lp.coeFn_add, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndL1Fin_ae_eq_condExpIndSMul]
  rw [condExpIndSMul]
  rw [indicatorConstLp_disjoint_union hs ht hμs hμt hst (1 : ℝ)]
  rw [map_add]
  push_cast
  rw [map_add]
  grw [Lp.coeFn_add]
  rfl

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsOrderedModule ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
hx : 0 ≤ x
⊢ 0 ≤ (condExpInd E hm μ s) x

Tactic:
rw [← coeFn_le]

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsOrderedModule ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
hx : 0 ≤ x
⊢ ↑↑0 ≤ᵐ[μ] ↑↑((condExpInd E hm μ s) x)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
have hs_g_eq : s_g =ᵐ[μ] Function.support g := hgm.ae_eq_mk.symm.support

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᵐ[μ] Function.support g
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)