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 ∈ 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? = some (-a.1, x).1
this : w'.head ∈ toSubgroup A B a.1
⊢ l ≠ []

Tactic:
rintro rfl

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
w' : NormalWord d
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
this : w'.head ∈ toSubgroup A B a.1
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) [a]
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := [], chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hx' : Option.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList.head? = some (-a.1, x).1
⊢ False
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
⊢ ¬Even ((card ∘ support) c)

Tactic:
comp_apply

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
⊢ ¬Even #c.support
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
⊢ Mul (PushoutI φ)

Tactic:
by
  delta PushoutI; infer_instance

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
⊢ One (PushoutI φ)

Tactic:
by
  delta PushoutI; infer_instance

Goal state after:
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
⊢ ⋯.leftQuotientEquiv ((op ↑h)⁻¹ • q) = ⋯.leftQuotientEquiv q

Tactic:
Equiv.apply_eq_iff_eq,

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
⊢ (op ↑h)⁻¹ • q = q
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
⊢ N ≠ ⊥

Tactic:
rintro rfl

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : ⊥.Normal
h1 : (Nat.card ↥⊥).Coprime ⊥.index
h3 : ∀ (H : Subgroup G), ¬⊥.IsComplement' H
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ (ofSubtype (u, v).1) (((noncommPiCoprod ⋯) (u, v).2) x) = (ofSubtype u) x

Tactic:
Equiv.apply_eq_iff_eq,

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((noncommPiCoprod ⋯) (u, v).2) x = x
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.index

Tactic:
← N.relIndex_top_right,

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.relIndex ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Nontrivial α
⊢ Nat.card ↥(alternatingGroup α) = 12

Tactic:
nat_card_alternatingGroup,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Nontrivial α
⊢ (Nat.card α).factorial / 2 = 12
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
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
x : PushoutI φ
g₁ : G i
hg₁ : (of i) g₁ = x
g₂ : G j
hg₂ : (of j) g₂ = x
hx : ¬x ∈ (base φ).range
⊢ x ≠ 1

Tactic:
rintro rfl

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
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
g₁ : G i
g₂ : G j
hg₁ : (of i) g₁ = 1
hg₂ : (of j) g₂ = 1
hx : ¬1 ∈ (base φ).range
⊢ False
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
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
g₁ : G i
g₂ : G j
hg₁ : (of i) g₁ = 1
hg₂ : (of j) g₂ = 1
hx : ¬1 ∈ (base φ).range
⊢ False

Tactic:
simp_all only [ne_eq, one_mem, not_true_eq_false]

Goal state after:
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 μβ
⊢ const α μβ = Kernel.sum fun n ↦ const α (sfiniteSeq μβ n)

Tactic:
rw [sum_const, sum_sfiniteSeq]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β), dist x x = 0

Tactic:
push_cast

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β), ↑(hammingDist (ofHamming x) (ofHamming x)) = 0
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β), dist x y = dist y x

Tactic:
push_cast

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (ofHamming x) (ofHamming y)) = ↑(hammingDist (ofHamming y) (ofHamming x))
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β), dist x z ≤ dist x y + dist y z

Tactic:
push_cast

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β),
    ↑(hammingDist (ofHamming x) (ofHamming z)) ≤
      ↑(hammingDist (ofHamming x) (ofHamming y)) + ↑(hammingDist (ofHamming y) (ofHamming z))
Module: Mathlib.Probability.Kernel.Basic

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

Tactic:
by
  ext1 a
  rw [Kernel.restrict_apply, Measure.restrict_univ]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔ ∃ ε > 0, ∀ {a b : Hamming β}, dist a b < ε → (a, b) ∈ s

Tactic:
push_cast

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔ ∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔ ∃ ε > 0, ∀ {a b : Hamming β}, dist a b < ε → (a, b) ∈ s

Tactic:
by
    push_cast
    constructor
    · refine fun hs ↦ ⟨1, zero_lt_one, fun hab ↦ hs <| by simpa using hab⟩
    · rintro ⟨_, hε, hs⟩ ⟨_, _⟩ rfl
      refine hs (lt_of_eq_of_lt ?_ hε)
      exact mod_cast hammingDist_self _

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ (Bornology.cobounded (Hamming β)).sets ↔ x✝ ∈ {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}

Tactic:
push_cast

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ ⊥.sets ↔ x✝ ∈ {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, ↑(hammingDist (ofHamming x) (ofHamming y)) ≤ C}
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
⊢ ∀ (x y : Hamming β), dist x y = ‖-x + y‖

Tactic:
push_cast

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (ofHamming x) (ofHamming y)) = ↑(hammingNorm (ofHamming (-x + y)))
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
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
⊢ ∃ η, ⇑κ =ᵐ[μ] ⇑η ∧ IsMarkovKernel η

Tactic:
obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using! measure_univ_le_add_compl s (μ := μ)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
a : α
ha : a ∈ sᶜ
⊢ ∃ η, ⇑κ =ᵐ[μ] ⇑η ∧ IsMarkovKernel η
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 β γ
inst✝¹ : IsMarkovKernel η
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
⊢ IsProbabilityMeasure ((η ∘ₖ κ) a)

Tactic:
comp_apply

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsMarkovKernel η
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
⊢ IsProbabilityMeasure ((κ a).bind ⇑η)
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
⊢ (Measure.dirac (f x.1)).prod (Measure.dirac (g x.2)) = Measure.dirac (f x.1, g x.2)

Tactic:
Measure.dirac_prod_dirac

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 : γ → δ
⊢ (η ∘ₖ κ).map f = η.map f ∘ₖ κ

Tactic:
by_cases hf : Measurable f
  · ext a s hs
    rw [map_apply' _ hf _ hs, comp_apply', comp_apply' _ _ _ hs]
    · simp_rw [map_apply' _ hf _ hs]
    · exact hf hs
  · simp [map_of_not_measurable _ hf]

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

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ ((swap γ β ∘ₖ (η ∥ₖ Kernel.id)) (MeasurableEquiv.prodAssoc.symm (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2)))
      s =
    (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
comp_apply

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ (((η ∥ₖ Kernel.id) (MeasurableEquiv.prodAssoc.symm (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2))).bind
        ⇑(swap γ β))
      s =
    (η (a, b)) (Prod.mk b ⁻¹' 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 η
f : β → δ
hf : Measurable f
⊢ κ.map f ×ₖ η = (κ ×ₖ η).map (Prod.map f id)

Tactic:
by
  rw [← map_prod_map _ _ hf measurable_id, map_id]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
⊢ Kernel.id ∥ₖ ξ ∘ₖ swap Z Y ∘ₖ (η ∥ₖ κ) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X

Tactic:
comp_assoc,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
⊢ Kernel.id ∥ₖ ξ ∘ₖ (swap Z Y ∘ₖ (η ∥ₖ κ)) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' 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 α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂κ x.1 ∂η x.2 = ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂η x.2 ∂κ x.1

Tactic:
refine (lintegral_lintegral_swap ?_).symm

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (Function.uncurry fun c b ↦ f (b, c)) ((κ x.1).prod (η x.2))
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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

Tactic:
simp [compProd_of_not_isSFiniteKernel_right _ _ hη]

Goal state after:
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 η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂η x ∂κ x = ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂κ x ∂η x

Tactic:
refine (lintegral_lintegral_swap ?_).symm

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (Function.uncurry fun c b ↦ f (b, c).swap) ((η x).prod (κ 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✝
⊢ ((Measure.dirac (f a✝¹)).prod (Measure.dirac (g a✝¹))) s✝ = (Measure.dirac (f a✝¹, g a✝¹)) s✝

Tactic:
Measure.dirac_prod_dirac

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ = ⇑η ∘ₘ ⇑(Kernel.deterministic Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ

Tactic:
comp_assoc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ = ⇑(η ∘ₖ Kernel.deterministic Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
⊢ MeasurableSet {a | Integrable f (κ a)}

Tactic:
simp_rw [Integrable, hf.aestronglyMeasurable, true_and]
  exact measurableSet_lt hf.enorm.lintegral_kernel measurable_const

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
b : Bool
⊢ (κ ∘ₖ boolKernel μ ν) b = (boolKernel (⇑κ ∘ₘ μ) (⇑κ ∘ₘ ν)) b

Tactic:
comp_apply

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
b : Bool
⊢ ⇑κ ∘ₘ (boolKernel μ ν) b = (boolKernel (⇑κ ∘ₘ μ) (⇑κ ∘ₘ ν)) b
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
⊢ (μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ

Tactic:
by
  rw [Measure.tilted, withDensity_apply' _ s]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂η b ∂κ a < ∞ ↔
    (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ∞) ∧
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal ∂κ a < ∞

Tactic:
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun h ↦ by
    rw [← and_congr_right_iff, and_iff_right_of_imp h]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂η b ∂κ a < ∞ ↔
    (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ∞) ∧
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal ∂κ a < ∞
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑↑(c • f) =ᵐ[μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

Tactic:
push_cast

Goal state after:
case refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑(c • ↑f) =ᵐ[μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)
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
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x))
          ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1) + (condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1))) =ᵐ[μ]
    ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm ht hμt x)

Tactic:
push_cast

Goal state after:
α : 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
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x))
          (↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) +
            ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)))) =ᵐ[μ]
    ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm ht hμt x)