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

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

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_range, sup_le_iff, noncommPiCoprod_range, iSup_le_iff]

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    ∀ (i : ↥g.cycleFactorsFinset), zpowers ↑i ≤ map (centralizer {g}).subtype (toPermHom g).ker
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τ⟩
hsign_k : sign ↑k = -1
⊢ False

Tactic:
by
    apply units_ne_neg_self (1 : ℤˣ)
    rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!

Tactic:
rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↑{h | IsConj g h} * Nat.card ↥(centralizer {g}) = (Fintype.card α)!
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
⊢ #(↑k).support = #c.support * 2

Tactic:
simp only [hk, toCentralizer, MonoidHom.coe_mk, OneHom.coe_mk, card_ofPermHom_support]

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
⊢ ∑ c ∈ τ.support, #(↑c).support = #c.support * 2
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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → g ∈ d.set j
⊢ h = 1

Tactic:
simp only [← (d.compl _).equiv_snd_eq_self_iff_mem (one_mem _)] at hw hφw
  have hhead : ((d.compl i).equiv (Word.equivPair i w).head).2 =
      (Word.equivPair i w).head := by
    rw [Word.equivPair_head]
    split_ifs with h
    · rcases h with ⟨_, rfl⟩
      exact hw _ _ (List.head_mem _)
    · rw [equiv_one (d.compl i) (one_mem _) (d.one_mem _)]
  by_contra hh1
  have := hφw i (φ i h * (Word.equivPair i w).head) ?_
  · apply hh1
    rw [equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩, hhead] at this
    simpa [((injective_iff_map_eq_one' _).1 (d.injective i))] using this
  · simp only [Word.mem_smul_iff, not_true, false_and, ne_eq, Option.mem_def, mul_right_inj,
      exists_eq_right', mul_eq_left, exists_prop, true_and, false_or]
    constructor
    · intro h
      apply_fun (d.compl i).equiv at h
      simp only [Prod.ext_iff, equiv_one (d.compl i) (one_mem _) (d.one_mem _),
        equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩, hhead, Subtype.ext_iff,
        Prod.ext_iff] at h
      rcases h with ⟨h₁, h₂⟩
      rw [h₂, coe_mul, ((d.compl i).coe_equiv_fst_eq_one_iff_mem (one_mem _)).mpr (d.one_mem _),
        mul_one, Subtype.coe_mk, map_eq_one_iff (φ i) (d.injective i)] at h₁
      contradiction
    · rw [Word.equivPair_head]
      dsimp
      split_ifs with hep
      · rcases hep with ⟨hnil, rfl⟩
        rw [head?_eq_some_head hnil]
        simp_all
      · push Not at hep
        by_cases hw : w.toList = []
        · simp [hw, Word.fstIdx]
        · simp [head?_eq_some_head hw, Word.fstIdx, hep hw]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)) ↔
    (↑((MulAut.conj ⟨g, hg⟩)⁻¹ ⟨k, hk⟩)).support ⊆ s ∧
      (↑((MulAut.conj ⟨g, hg⟩)⁻¹ ⟨k, hk⟩) = 1 ∨ (↑((MulAut.conj ⟨g, hg⟩)⁻¹ ⟨k, hk⟩)).cycleType = {2, 2})

Tactic:
MulAut.inv_apply,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)) ↔
    (↑((MulEquiv.symm (MulAut.conj ⟨g, hg⟩)) ⟨k, hk⟩)).support ⊆ s ∧
      (↑((MulEquiv.symm (MulAut.conj ⟨g, hg⟩)) ⟨k, hk⟩) = 1 ∨
        (↑((MulEquiv.symm (MulAut.conj ⟨g, hg⟩)) ⟨k, hk⟩)).cycleType = {2, 2})
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
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
⊢ kleinFour α = commutator ↥(alternatingGroup α)

Tactic:
refine le_antisymm ?_ comm_le
    intro g hg
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4,
      Set.mem_union, Set.mem_singleton_iff, Set.mem_ofPred_eq] at hg
    rcases hg with ⟨rfl⟩ | hg
    · exact Subgroup.one_mem _
    · rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
      obtain ⟨c, hc⟩ := hk22
      rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
      simp only [commutator, ← hc]
      let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c
      suffices (⊤ : Subgroup (alternatingGroup α)) =
        Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
        rw [this, ← Subgroup.map_commutator]
        refine Subgroup.mem_map_of_mem _ hk
      simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ ⊤ ≤ ⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s)

Tactic:
← closure_cycleType_eq_two_two_eq_top h5,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ closure {g | (↑g).cycleType = {2, 2}} ≤ ⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s)
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
a : α
⊢ IsZeroOrProbabilityMeasure (κ a)

Tactic:
by
  rcases eq_zero_or_isMarkovKernel κ with rfl | h'
  · simp only [zero_apply]
    infer_instance
  · infer_instance

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

Goal state before:
pp: case inl
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 : ↑P ≤ f'.ker
⊢ IsCyclic ↥↑P

Tactic:
replace h_le : P ≤ f.range := h.trans h_le
    suffices IsCyclic (P.subgroupOf f.range) by
      have key := Subgroup.subgroupOfEquivOfLe h_le
      exact isCyclic_of_surjective key key.surjective
    obtain ⟨Q, hQ⟩ := Sylow.mapSurjective_surjective f.rangeRestrict_surjective p (P.subtype h_le)
    rw [Sylow.ext_iff, Sylow.coe_mapSurjective, Sylow.coe_subtype] at hQ
    exact hQ ▸ isCyclic_of_surjective _ (f.rangeRestrict.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 α β
y' y : α
hy' : y' ∈ measurableAtom y
s : Set β
hs : MeasurableSet s
⊢ (κ y') s = (κ y) s

Tactic:
exact mem_of_mem_measurableAtom hy' (κ.measurable_coe hs (measurableSet_singleton (κ y s))) rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ (Measure.comap f (κ a)) t = (κ a) (f '' t)

Tactic:
Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ (κ a) (f '' t) = (κ a) (f '' t)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
⊢ IsMarkovKernel (κ.comapRight hf)

Tactic:
by
  refine ⟨fun a => ⟨?_⟩⟩
  rw [comapRight_apply' κ hf a MeasurableSet.univ]
  simp only [Set.image_univ]
  exact hκ a

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

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

Tactic:
by
  ext a
  simp [map_apply, measurable_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (Measure.map Prod.swap (κ a)) s = (κ a) {p | p.swap ∈ s}

Tactic:
Measure.map_apply measurable_swap hs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ a) (Prod.swap ⁻¹' s) = (κ a) {p | p.swap ∈ s}
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
a : α
⊢ ((κ ×ₖ η) a) (s ×ˢ t) = (κ a) s * (η a) t

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
a : α
⊢ ((κ a).prod (η a)) (s ×ˢ t) = (κ a) s * (η a) t
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
x : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((const α μ ×ₖ const α ν) x) s✝ = (μ.prod ν) s✝

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
x : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ (((const α μ) x).prod ((const α ν) x)) s✝ = (μ.prod ν) s✝
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η) a = ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂κ a ∂η a

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ a).prod (η a) = ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂κ a ∂η a
Module: Mathlib.Probability.Kernel.Composition.Prod

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 β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ (κ ×ₖ η) (f x) = (κ.comap f hf ×ₖ η.comap f hf) x

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ (κ (f x)).prod (η (f x)) = (κ.comap f hf ×ₖ η.comap f hf) x
Module: Mathlib.Probability.Kernel.Composition.Prod

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 β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ (κ (f x)).prod (η (f x)) = (κ.comap f hf ×ₖ η.comap f hf) x

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ (κ (f x)).prod (η (f x)) = ((κ.comap f hf) x).prod ((η.comap f hf) x)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α δ
inst✝ : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
⊢ (κ.map f ×ₖ η.map g) x = (Measure.map f (κ x)).prod (Measure.map g (η x))

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α δ
inst✝ : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
⊢ ((κ.map f) x).prod ((η.map g) x) = (Measure.map f (κ x)).prod (Measure.map g (η x))
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a✝¹ : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((deterministic f hf ×ₖ deterministic g hg) a✝¹) s✝ = ((deterministic (fun a ↦ (f a, g a)) ⋯) a✝¹) s✝

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a✝¹ : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ (((deterministic f hf) a✝¹).prod ((deterministic g hg) a✝¹)) s✝ = ((deterministic (fun a ↦ (f a, g a)) ⋯) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.Prod

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 α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ Measure.map (⇑MeasurableEquiv.prodAssoc) ((κ ×ₖ ξ ×ₖ η) a) = (κ ×ₖ (ξ ×ₖ η)) a

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ Measure.map (⇑MeasurableEquiv.prodAssoc) (((κ ×ₖ ξ) a).prod (η a)) = (κ ×ₖ (ξ ×ₖ η)) a
Module: Mathlib.Probability.Kernel.Composition.Prod

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 α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ Measure.map (⇑MeasurableEquiv.prodAssoc) (((κ ×ₖ ξ) a).prod (η a)) = (κ ×ₖ (ξ ×ₖ η)) a

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ Measure.map (⇑MeasurableEquiv.prodAssoc) (((κ a).prod (ξ a)).prod (η a)) = (κ ×ₖ (ξ ×ₖ η)) a
Module: Mathlib.Probability.Kernel.Composition.Prod

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 α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ (κ a).prod ((ξ a).prod (η a)) = (κ ×ₖ (ξ ×ₖ η)) a

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ (κ a).prod ((ξ a).prod (η a)) = (κ a).prod ((ξ ×ₖ η) a)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
μ : Measure γ
inst✝¹ : SFinite μ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
⊢ ∫⁻ (b : β), ((const β μ ×ₖ η) b) s ∂κ x = ((const α μ ×ₖ (η ∘ₖ κ)) x) s

Tactic:
prod_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
μ : Measure γ
inst✝¹ : SFinite μ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
⊢ ∫⁻ (b : β), (((const β μ) b).prod (η b)) s ∂κ x = (((const α μ) x).prod ((η ∘ₖ κ) x)) s
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
μ : Measure γ
inst✝¹ : SFinite μ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
⊢ ∫⁻ (b : β), ∫⁻ (y : δ), μ ((fun x ↦ (x, y)) ⁻¹' s) ∂η b ∂κ x = ∫⁻ (y : δ), μ ((fun x ↦ (x, y)) ⁻¹' s) ∂(η ∘ₖ κ) x

Tactic:
lintegral_comp _ _ _ (measurable_measure_prodMk_right ms)

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

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : 𝓧
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ (ν univ)⁻¹ * (ν univ * μ.rnDeriv ν x) = μ.rnDeriv ν x

Tactic:
rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]

Goal state after:
case h0
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : 𝓧
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ ν univ ≠ 0

case ht
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : 𝓧
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ ν univ ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀ _ _ hs]
    · congr
    · suffices AEMeasurable (fun x ↦ exp (f x) / ∫ x, exp (f x) ∂μ) μ by
        rw [← aemeasurable_coe_nnreal_real_iff]
        refine AEMeasurable.restrict ?_
        simpa only [NNReal.coe_mk]
      exact (measurable_exp.comp_aemeasurable hf).div_const _

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

Goal state before:
pp: ⊢ Continuous klFun

Tactic:
unfold klFun

Goal state after:
⊢ Continuous fun x ↦ x * log x + 1 - x
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ ¬DifferentiableAt ℝ klFun 0

Tactic:
unfold klFun

Goal state after:
⊢ ¬DifferentiableAt ℝ (fun x ↦ x * log x + 1 - x) 0
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ∞

Tactic:
by
  rw [klDiv_def]
  exact if_neg (not_and_of_not_right _ h)

Goal state after: