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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : (List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList).head? = Option.map Prod.fst (some (-a.1, x))
⊢ False

Tactic:
List.head?_map,

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head? = Option.map Prod.fst (some (-a.1, x))
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (↑(↑τ).support).PairwiseDisjoint fun c ↦ (↑c).support

Tactic:
intro c

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
⊢ c ∈ ↑(↑τ).support →
    ∀ ⦃y : ↥g.cycleFactorsFinset⦄, y ∈ ↑(↑τ).support → c ≠ y → Function.onFun _root_.Disjoint (fun c ↦ (↑c).support) c y
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ ∀ (x : ↥g.cycleFactorsFinset), ((OnCycleFactors.toPermHom g) (a.toCentralizer τ)) x = ↑τ x

Tactic:
intro c

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
⊢ ((OnCycleFactors.toPermHom g) (a.toCentralizer τ)) c = ↑τ c
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
⊢ ResiduallyFinite G

Tactic:
rw [residuallyFinite_iff_exists_finiteIndex]

Goal state after:
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
⊢ ∀ (g : G), g ≠ 1 → ∃ H, H.FiniteIndex ∧ g ∉ H
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
this : -(-1) ^ #c.support = 1
⊢ Odd ((card ∘ support) c)

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : sign c = 1
⊢ c.IsCycle

Tactic:
neg_eq_iff_eq_neg,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : (-1) ^ #c.support = -1
⊢ Odd ((card ∘ support) c)

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : sign c = 1
⊢ c.IsCycle
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
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ⟨(unop g)⁻¹ * ↑1 * unop g, ⋯⟩ = 1

Tactic:
Subtype.ext_iff,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ↑⟨(unop g)⁻¹ * ↑1 * unop g, ⋯⟩ = ↑1
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 : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ * h

Tactic:
Subtype.ext_iff,

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.PushoutI

Goal state before:
pp: case H.inl.mul
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive ↑(inl x)
ihy : motive ↑(inl y)
⊢ motive ↑(inl (x * y))

Tactic:
map_mul

Goal state after:
case H.inl.mul
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive ↑(inl x)
ihy : motive ↑(inl y)
⊢ motive ↑(inl x * inl y)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
⊢ ↑p ∈ (kerParam g).range

Tactic:
simp only [SetLike.mem_coe, mem_ker_toPermHom_iff, IsCycle.forall_commute_iff] at hp

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), ↑p x ∈ c.support ↔ x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
⊢ ↑p ∈ (kerParam g).range
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 : ι
w₁ : Word G
h₁ : H
hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
h : w₁ = (CoprodI.of ((φ i) h₁))⁻¹ • CoprodI.of ((φ i) h₂) • w₂
⊢ { toWord := w₁, head := h₁, normalized := hw₁ } = { toWord := w₂, head := h₂, normalized := hw₂ }

Tactic:
← mul_smul

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
w₁ : Word G
h₁ : H
hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
h : w₁ = ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂
⊢ { toWord := w₁, head := h₁, normalized := hw₁ } = { toWord := w₂, head := h₂, normalized := hw₂ }
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
⊢ ∃ H, N.IsComplement' H

Tactic:
by_cases hN1 : Nat.card N = 0
  · rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN
    rw [hN]
    exact ⟨⊥, isComplement'_top_bot⟩
  by_cases hN2 : N.index = 0
  · rw [hN2, Nat.coprime_zero_right, Nat.card_eq_one_iff_unique] at hN
    have := hN.1
    rw [N.eq_bot_of_subsingleton]
    exact ⟨⊤, isComplement'_bot_top⟩
  have hN3 : Finite G := by
    apply Nat.finite_of_card_ne_zero
    rw [← N.card_mul_index]
    exact mul_ne_zero hN1 hN2
  exact exists_right_complement'_of_coprime_aux' rfl hN

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ Monoid.exponent ↥(kleinFour α) ∣ 2

Tactic:
Monoid.exponent_dvd

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ ∀ (g : ↥(kleinFour α)), orderOf g ∣ 2
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ ∀ (a : QuaternionGroup n), a.inv * a = 1

Tactic:
rintro (i | i)
    · exact congr_arg a (neg_add_cancel i)
    · exact congr_arg a (sub_self (n + i))

Goal state after:
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
⊢ (g • w).prod = (of i) g * w.prod

Tactic:
by
  simp only [prod, summand_smul_def', equivPair, rcons, Word.equivPair_symm,
    Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk, Word.equivPair_smul_same,
    Word.equivPair_tail_eq_inv_smul, Word.rcons_eq_smul, ← of_apply_eq_base φ i,
    MonoidHom.apply_ofInjective_symm, equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv,
    Word.prod_smul, ofCoprodI_of, inv_mul_cancel_left, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case base
ι : 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)
h : H
w : NormalWord d
a✝ : w.head = 1
ih : w.prod • empty = w
⊢ ((base φ) h • w).prod • empty = (base φ) h • w

Tactic:
| base h w _ ih =>

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''
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
h_le : ↑P ≤ f.range
⊢ IsCyclic ↥↑P

Tactic:
suffices IsCyclic (P.subgroupOf f.range) by
      have key := Subgroup.subgroupOfEquivOfLe h_le
      exact isCyclic_of_surjective key key.surjective

Goal state after:
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''
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
h_le : ↑P ≤ f.range
⊢ IsCyclic ↥((↑P).subgroupOf f.range)
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 ν
⊢ ∃ κs, (∀ (n : ℕ), IsFiniteKernel (κs n)) ∧ boolKernel μ ν = Kernel.sum κs

Tactic:
refine ⟨fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n), fun n ↦ inferInstance, ?_⟩

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

Goal state before:
pp: case refine_1
α : 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 : ℕ
⊢ ∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s),
    Measurable fun a ↦
      ∫⁻ (b : β), (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0)) (a, b) ∂κ a

Tactic:
intro c

Goal state after:
case refine_1
α : 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 : ℕ
c : ℝ≥0∞
⊢ ∀ {s : Set (α × β)} (hs : MeasurableSet s),
    Measurable fun a ↦
      ∫⁻ (b : β), (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0)) (a, b) ∂κ a
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 δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)

Tactic:
have : (fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s))
          = fun y ↦ prodMkRight β (prodMkLeft α η) y (Prod.mk y.2 ⁻¹' s) := rfl

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  (fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)) = fun y ↦
    ((prodMkRight β (prodMkLeft α η)) y) (Prod.mk y.2 ⁻¹' s)
⊢ Measurable fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, (F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), (F n) (b, c) ∂η (a, b)
h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b ↦ ∫⁻ (c : γ), f' (b, c) ∂η (a, b)
n : ℕ
⊢ ∀ (c : ℝ≥0∞) {s : Set (β × γ)} (hs : MeasurableSet s),
    ∫⁻ (a : β × γ),
        (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0)) a ∂(κ ⊗ₖ η) a =
      ∫⁻ (a_1 : β),
        ∫⁻ (c_1 : γ),
          (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0))
            (a_1, c_1) ∂η (a, a_1) ∂κ a

Tactic:
intro c

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, (F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), (F n) (b, c) ∂η (a, b)
h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b ↦ ∫⁻ (c : γ), f' (b, c) ∂η (a, b)
n : ℕ
c : ℝ≥0∞
⊢ ∀ {s : Set (β × γ)} (hs : MeasurableSet s),
    ∫⁻ (a : β × γ),
        (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0)) a ∂(κ ⊗ₖ η) a =
      ∫⁻ (a_1 : β),
        ∫⁻ (c_1 : γ),
          (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0))
            (a_1, c_1) ∂η (a, a_1) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ ∀ (c : E) ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      ((κ ⊗ₖ η) a) s < ∞ →
        ∫ (z : β × γ), s.indicator (fun x ↦ c) z ∂(κ ⊗ₖ η) a =
          ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) (x, y) ∂η (a, x) ∂κ a

Tactic:
intro c

Goal state after:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
⊢ ∀ ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      ((κ ⊗ₖ η) a) s < ∞ →
        ∫ (z : β × γ), s.indicator (fun x ↦ c) z ∂(κ ⊗ₖ η) a =
          ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) (x, y) ∂η (a, x) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable f ((κ ⊗ₖ η) a)
A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a
B : ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a = ∫⁻ (x : β), ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂η (a, x) ∂κ a
⊢ Measurable (AEMeasurable.mk f hf)

Tactic:
exact hf.measurable_mk

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (fun x ↦ rexp (f x)) μ

Tactic:
suffices ¬ AEMeasurable (fun x ↦ exp (f x)) μ by exact fun h ↦ this h.1.aemeasurable

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable (fun x ↦ rexp (f x)) μ
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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
simp_rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht,
    lintegral_compProd _ _ _ hf, Kernel.restrict_apply]

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

Goal state before:
pp: case refine_1
α : 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
g : ↥(Lp E 1 ((η ∘ₖ κ) a))
this : ∀ (i : ↥(Lp E 1 ((η ∘ₖ κ) a))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i y - ↑↑g y‖ₑ ∂η x ∂κ a) (𝓝 g) (𝓝 0)

Tactic:
simp_rw [← lintegral_comp _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]

Goal state after:
case refine_1
α : 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
g : ↥(Lp E 1 ((η ∘ₖ κ) a))
this : ∀ (i : ↥(Lp E 1 ((η ∘ₖ κ) a))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind
α : 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
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ (c : E) ⦃s : Set γ⦄,
    MeasurableSet s →
      ((η ∘ₖ κ) a) s < ∞ →
        ∫ (z : γ), s.indicator (fun x ↦ c) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) y ∂η x ∂κ a

Tactic:
intro c

Goal state after:
case pos.h_ind
α : 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
f✝ : γ → E
hE : CompleteSpace E
c : E
⊢ ∀ ⦃s : Set γ⦄,
    MeasurableSet s →
      ((η ∘ₖ κ) a) s < ∞ →
        ∫ (z : γ), s.indicator (fun x ↦ c) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) y ∂η x ∂κ a
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ∨ (μ.rnDeriv ν x).toReal = 0

Tactic:
exact Or.inl (by positivity)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
x : α
hx : (μ.tilted f).rnDeriv ν x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ∨ (μ.rnDeriv ν x).toReal = 0

Tactic:
exact Or.inl (by positivity)

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ klFun x = 0 ↔ x = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [klFun_apply, h]⟩

Goal state after:
x : ℝ
hx : 0 ≤ x
h : klFun x = 0
⊢ x = 1
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : μ univ = ν univ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

Tactic:
by
  by_cases h_int : Integrable (llr μ ν) μ
  · simp [toReal_klDiv h h_int, h_eq, measureReal_def]
  · rw [klDiv_of_not_integrable h_int, integral_undef h_int, ENNReal.toReal_top]

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
⊢ μ = c • c⁻¹ • μ

Tactic:
rw [smul_smul, mul_inv_cancel₀ hc, one_smul]

Goal state after: