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

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

Tactic:
rw [hb']

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 b = a then f a else b) = b
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite (IteratedWreathProduct G n)

Tactic:
induction n with
  | zero => rw [IteratedWreathProduct_zero]; infer_instance
  | succ n h => rw [IteratedWreathProduct_succ]; infer_instance

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (of i) ((φ i) x) = (base φ) x

Tactic:
← MonoidHom.comp_apply,

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ((of i).comp (φ i)) x = (base φ) x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ map (centralizer {g}).subtype (toPermHom g).ker ≤ (kerParam g).range

Tactic:
rintro - ⟨p, hp, rfl⟩

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
⊢ (centralizer {g}).subtype p ∈ (kerParam g).range
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ #{g | (↑g).cycleType = {n}} = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
← card_map,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ #(map ?m.50 {g | (↑g).cycleType = {n}}) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ ↥(alternatingGroup α) ↪ ?m.48

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ Type ?u.47
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card ↑(Function.fixedPoints ⇑g))! * ∏ i, Fintype.card ↥(zpowers ↑i) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
card_fixedPoints

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card α - g.cycleType.sum)! * ∏ i, Fintype.card ↥(zpowers ↑i) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign ((noncommPiCoprod ⋯) ((k, v).1, (k, v).2).2) = ∏ c ∈ g.cycleFactorsFinset.attach, sign ↑(v c)

Tactic:
← MonoidHom.comp_apply,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ (sign.comp (noncommPiCoprod ⋯)) ((k, v).1, (k, v).2).2 = ∏ c ∈ g.cycleFactorsFinset.attach, sign ↑(v c)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign ((kerParam g) (k, v)) = sign k * ∏ c, sign ↑(v c)

Tactic:
by
  rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one,
    one_mul, map_mul, sign_ofSubtype, Finset.univ_eq_attach, mul_right_inj, ← MonoidHom.comp_apply,
    Subgroup.noncommPiCoprod, MonoidHom.comp_noncommPiCoprod _, MonoidHom.noncommPiCoprod_apply,
    Finset.univ_eq_attach, Finset.noncommProd_eq_prod]
  simp

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
that : (↑k).cycleType.card = #c.support
⊢ #c.support ∈ g.cycleType

Tactic:
simp only [cycleType_def, Multiset.mem_map]

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
that : (↑k).cycleType.card = #c.support
⊢ ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = #c.support
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
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ (of i) g • w = g • w

Tactic:
rw [summand_smul_def, summand_smul_def']

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case e'_9
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ (φ i) 1 = (φ i) (NormalWord.cons g { toWord := w, head := 1, normalized := ⋯ } h1 ?cons).head

Tactic:
simp only [NormalWord.cons, equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm,
          map_one, mul_one, mul_inv_cancel, (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]

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

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
⊢ False

Tactic:
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 1)) = 0
⊢ False

Tactic:
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : orderOf (a 1) = 0
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ IsCyclic ↥⁅⊤, ⊤⁆

Tactic:
induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH
   =>  _ 

Goal state after:
case ind
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⁅H, H⁆
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
f : Perm α
hf : f.IsThreeCycle
⊢ normalClosure {⟨f, ⋯⟩} = ⊤

Tactic:
have : IsSimpleGroup (alternatingGroup α) := isSimpleGroup h5
  apply normalClosure_normal.eq_bot_or_eq_top.resolve_left
  simp [hf.ne_one]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
this : IsCyclic ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥(Subgroup.map H.subtype (commutator ↥H)) := (commutator ↥H).equivMapOfInjective H.subtype ⋯
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
rw [Subgroup.map_subtype_commutator] at f

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
this : IsCyclic ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆
⊢ IsCyclic ↥⁅H, H⁆
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ + η)

Tactic:
by
  refine ⟨⟨κ.bound + η.bound, ENNReal.add_lt_top.mpr ⟨κ.bound_lt_top, η.bound_lt_top⟩, fun a => ?_⟩⟩
  exact add_le_add (Kernel.measure_le_bound _ _ _) (Kernel.measure_le_bound _ _ _)

Goal state after:
Module: Mathlib.InformationTheory.Hamming

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

Tactic:
rw [hammingDist, card_eq_zero, filter_eq_empty_iff]
  exact fun _ _ H => H rfl

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : 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
⊢ (hammingDist (fun i ↦ f i (x i)) fun i ↦ f i (y i)) ≤ hammingDist x y

Tactic:
dsimp [hammingDist]; gcongr; simp +contextual

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comapRight ⋯ = κ

Tactic:
ext _ _ hs; rw [comapRight_apply' _ _ _ hs]; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun y ↦ (η y) t) =ᵐ[κ a] 0
⊢ (fun x ↦ (η x) s) =ᵐ[κ a] 0

Tactic:
Filter.eventuallyLE_antisymm_iff

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun y ↦ (η y) t) =ᵐ[κ a] 0
⊢ (fun x ↦ (η x) s) ≤ᵐ[κ a] 0 ∧ 0 ≤ᵐ[κ a] fun x ↦ (η x) s
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ ∀ ⦃f g : SimpleFunc (α × β) ℝ≥0∞⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (Measurable fun a ↦ ∫⁻ (b : β), f (a, b) ∂κ a) →
        (Measurable fun a ↦ ∫⁻ (b : β), g (a, b) ∂κ a) → Measurable fun a ↦ ∫⁻ (b : β), (f + g) (a, b) ∂κ a

Tactic:
· intro g₁ g₂ _ hm₁ hm₂
    simp only [SimpleFunc.coe_add, Pi.add_apply]
    have h_add :
      (fun a => ∫⁻ b, g₁ (a, b) + g₂ (a, b) ∂κ a) =
        (fun a => ∫⁻ b, g₁ (a, b) ∂κ a) + fun a => ∫⁻ b, g₂ (a, b) ∂κ a := by
      ext1 a
      rw [Pi.add_apply, lintegral_add_left (by fun_prop)]
    rw [h_add]
    exact Measurable.add hm₁ hm₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a ↦ ∫⁻ (b : β) in s, f a b ∂κ a

Tactic:
simp_rw [← lintegral_restrict κ hs]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a ↦ ∫⁻ (b : β), f a b ∂(κ.restrict hs) a
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (a : β) in s, f a b ∂κ b

Tactic:
simp_rw [← lintegral_restrict κ hs]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (a : β), f a b ∂(κ.restrict hs) b
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

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

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

Tactic:
· rw [compProd_of_not_sfinite _ _ hμ]; simp

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

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

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
· rw [compProd_of_not_sfinite _ _ hμ]; simp

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
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 γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
⊢ ((κ ⊗ₖ η) x) (Prod.fst ⁻¹' s) = (κ x) s

Tactic:
simp_rw [compProd_apply (measurable_fst hs), ← Set.preimage_comp, Prod.fst_comp_mk, Set.preimage,
    Function.const_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
⊢ ∫⁻ (b : β), (η (x, b)) {x | b ∈ s} ∂κ x = (κ x) s
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 γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ∞

Tactic:
Kernel.compProd_apply ht

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' t) ∂κ a ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ∞
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 γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' t)) =ᵐ[κ a] 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0

Tactic:
Filter.eventuallyLE_antisymm_iff

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' t)) =ᵐ[κ a] 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) ≤ᵐ[κ a] 0 ∧ 0 ≤ᵐ[κ a] fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : μ Set.univ = ∞
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

Tactic:
simp only [measureReal_def, h_univ, ENNReal.toReal_top, zero_mul, div_zero,
      ENNReal.ofReal_zero, zero_smul, ENNReal.inv_top]

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
⊢ (μ.rnDeriv ν x).toReal = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
⊢ 0 < (μ.rnDeriv ν x).toReal

Tactic:
if_neg h_zero

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
⊢ (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
⊢ 0 < (μ.rnDeriv ν x).toReal
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x) μ ↔
    Integrable (fun x ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ

Tactic:
congr! with a
    rw [ENNReal.toReal_ofReal]
    positivity

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

Goal state before:
pp: α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ eLpNorm' f q (μ.trim hm) = eLpNorm' f q μ

Tactic:
simp_rw [eLpNorm']
  congr 1
  exact lintegral_trim hm (by fun_prop)

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

Goal state before:
pp: α : 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 • ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr (c⁻¹ • μ) ν) μ

Tactic:
rw [integrable_congr (llr_smul_nnreal_left hμν c⁻¹ (by simpa))]

Goal state after:
α : 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 • ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ llr μ ν x + log ↑c⁻¹) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ (condExpL1CLM F' hm μ) (c • f) = c • (condExpL1CLM F' hm μ) f

Tactic:
refine L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f
  exact fun c s x => condExpInd_smul' c x

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

Goal state before:
pp: case refine_1
α : 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 : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
f : α → F
hf : MemLp f p μ
hfm : AEStronglyMeasurable f μ
f_Lp : ↥(Lp F p μ) := toLp f hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
⊢ ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑↑↑(Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)

Tactic:
intro c s hs hμs
    rw [Lp.simpleFunc.coe_indicatorConst]
    refine h_ae indicatorConstLp_coeFn.symm ?_ (h_ind c hs hμs)
    exact memLp_indicator_const p (hm s hs) c (Or.inr hμs.ne)

Goal state after: