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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬toPerm g = 1
a : α
ha : g • a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g • a ∉ s
⊢ ¬toPerm g = 1

Tactic:
Equiv.ext_iff,

Goal state after:
case refine_1
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬toPerm g = 1
a : α
ha : g • a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g • a ∉ s
⊢ ¬∀ (x : ↑(powersetCard α n)), (toPerm g) x = 1 x
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ ↑(ofFinEmb n α (g • f)) = ↑(id g • ofFinEmb n α f)

Tactic:
coe_smul,

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ ↑(ofFinEmb n α (g • f)) = id g • ↑(ofFinEmb n α f)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : fixedPoints G ↑(powersetCard α n) = univ
⊢ g = 1

Tactic:
replace h : (toPerm g : Perm (powersetCard α n)) = 1 := by
    ext1 s
    exact eq_univ_iff_forall.mp h s g

Goal state after:
G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : toPerm g = 1
⊢ g = 1
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
this : finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M
⊢ finrank ℤ M ≤ finrank ℤ ↥A

Tactic:
rw [← this]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
this : finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M
⊢ finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range ≤ finrank ℤ ↥A
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯
⊢ (S.subtype.comp f) HNNExtension.t = (MonoidHom.id (HNNExtension G A B φ)) HNNExtension.t

Tactic:
by simp [f]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ comap f K ≤ normalizer ↑(comap f H)

Tactic:
exact (comap_mono hN).trans (le_normalizer_comap f)

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels u w
⊢ ReducedWord.prod φ
      (let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord

Tactic:
simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv]
    rcases Int.units_eq_one_or u with (rfl | rfl)
    · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
      -- simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul].
      simp only [toSubgroup_neg_one, toSubgroup_one, toSubgroupEquiv_one, equiv_eq_conj, mul_assoc,
        Units.val_one, zpow_one, inv_mul_cancel_left, mul_right_inj]
      erw [(d.compl 1).equiv_snd_eq_inv_mul]
      simp [mul_assoc]
    · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
      -- simp [equiv_symm_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul]
      simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
        Int.reduceNeg, zpow_neg, zpow_one, mul_assoc]
      erw [equiv_symm_eq_conj, (d.compl (-1)).equiv_snd_eq_inv_mul]
      simp [mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset

Tactic:
have := cycleFactorsFinset_conj_eq (ConjAct.toConjAct (k : Perm α)) g

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : (ConjAct.toConjAct k • g).cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
⊢ (∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
      ((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset) k) ⟨a, b⟩ = 1 ⟨a, b⟩) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c

Tactic:
refine forall₂_congr (fun _ _ ↦ ?_)

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
x✝¹ : Perm α
x✝ : x✝¹ ∈ g.cycleFactorsFinset
⊢ ((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset) k) ⟨x✝¹, x✝⟩ = 1 ⟨x✝¹, x✝⟩ ↔ Commute (↑k) x✝¹
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ¬∃ a ∈ (↑τ).support, x ∈ (↑a).support

Tactic:
rintro ⟨c, -, hc⟩

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
⊢ False
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝ : Finite Q
⊢ Nat.card ((Q → D) × Q) = Nat.card D ^ Nat.card Q * Nat.card Q

Tactic:
Nat.card_prod (Q → D) Q,

Goal state after:
D : Type u_1
Q : Type u_2
inst✝ : Finite Q
⊢ Nat.card (Q → D) * Nat.card Q = Nat.card D ^ Nat.card Q * Nat.card Q
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✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
⊢ Nat.card (Fin n → G) = p ^ n

Tactic:
rw [Nat.card_fun, Nat.card_fin, hG]

Goal state after:
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✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : IteratedWreathProduct G n →* Equiv.Perm α := e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf : Function.Injective ⇑f
g : ↥f.range ≃* IteratedWreathProduct G n := (MonoidHom.ofInjective hf).symm
⊢ Nat.card ↥f.range = p ^ (Nat.card (Equiv.Perm α)).factorization p

Tactic:
rw [Nat.card_congr g.toEquiv, IteratedWreathProduct.card, hG, Nat.card_perm, hα,
        ← Nat.multiplicity_eq_factorization hp.out (p ^ n).factorial_ne_zero,
        Nat.Prime.multiplicity_factorial_pow hp.out]

Goal state after:
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'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index

Tactic:
index_map

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'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime N.index
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case cons
ι : 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 φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
⊢ ∃ w',
    w'.prod = ofCoprodI (Word.cons g w hIdx hg1).prod ∧
      List.map Sigma.fst w'.toList = List.map Sigma.fst (Word.cons g w hIdx hg1).toList

Tactic:
rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with
      ⟨w', hw'prod, hw'map⟩

Goal state after:
case cons
ι : 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 φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ ∃ w',
    w'.prod = ofCoprodI (Word.cons g w hIdx hg1).prod ∧
      List.map Sigma.fst w'.toList = List.map Sigma.fst (Word.cons g w hIdx hg1).toList
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⁆
h : Abelianization.of.ker ≤ Subgroup.center ↥(commutator ↥H)
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
let _ := commGroupOfCyclicCenterQuotient Abelianization.of h

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⁆
h : Abelianization.of.ker ≤ Subgroup.center ↥(commutator ↥H)
x✝ : CommGroup ↥(commutator ↥H) := commGroupOfCyclicCenterQuotient Abelianization.of h
⊢ IsCyclic ↥(commutator ↥H)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ Measure.comap f (κ a) = Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)

Tactic:
have :
    (Measure.sum fun n => Measure.comap f (seq κ n a)) =
      Measure.comap f (Measure.sum fun n => seq κ n a) := by
    ext1 t ht
    rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht,
      Measure.sum_apply _ ht, Measure.sum_apply _ (hf.measurableSet_image.mpr ht)]
    congr with n : 1
    rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
this : (Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)) = Measure.comap f (Measure.sum fun n ↦ (κ.seq n) a)
⊢ Measure.comap f (κ a) = Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
⊢ ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)

Tactic:
by
  refine ext_fun fun a f hf => ?_
  simp_rw [lintegral_comp _ _ _ hf, lintegral_comp _ _ _ hf.lintegral_kernel]

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

Goal state before:
pp: case hf
α : 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
a : α
⊢ ∀ (n : ℕ), Measurable fun b ↦ (F n) (a, b)

pp: case h_mono
α : 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
a : α
⊢ Monotone fun n b ↦ (F n) (a, b)

Tactic:
· exact fun n => (F n).measurable.comp measurable_prodMk_left

Goal state after:
case h_mono
α : 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
a : α
⊢ Monotone fun n b ↦ (F n) (a, b)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ μ ⊗ₘ κ = 0

Tactic:
by
  rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_left, zero_apply]
  rwa [Kernel.isSFiniteKernel_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Kernel.id.comap f hf = deterministic f hf

Tactic:
ext
  rw [Kernel.comap_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
⊢ (Kernel.sum fun i ↦ prodMkRight γ (κ i)) = prodMkRight γ (Kernel.sum κ)

Tactic:
by
  ext
  simp_rw [sum_apply, prodMkRight_apply, sum_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (Kernel.prodMkLeft γ κ)

Tactic:
rw [Kernel.prodMkLeft]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.snd ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (Kernel.prodMkLeft γ κ)

Tactic:
rw [Kernel.prodMkLeft]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap Prod.snd ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (Kernel.prodMkLeft γ κ)

Tactic:
rw [Kernel.prodMkLeft]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.snd ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (Kernel.prodMkLeft γ κ)

Tactic:
rw [Kernel.prodMkLeft]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.snd ⋯)
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 γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero ((κ.sectL b) a)

Tactic:
rw [sectL_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero (κ (a, b))
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

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

Tactic:
by
  by_cases hμ : SFinite μ
  swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp
  by_cases hν : SFinite ν
  swap; · rw [compProd_of_not_sfinite _ _ hν]; simp
  by_cases hκ : IsSFiniteKernel κ
  swap; · rw [compProd_of_not_isSFiniteKernel _ _ hκ]; simp
  by_cases hη : IsSFiniteKernel η
  swap; · rw [compProd_of_not_isSFiniteKernel _ _ hη]; simp
  refine ⟨hμν.nullSet ×ˢ univ, hμν.measurableSet_nullSet.prod .univ, ?_⟩
  rw [compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union]
  simp only [MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ,
    prod_empty, union_empty, true_and]
  rw [compProd_apply_prod hμν.measurableSet_nullSet.compl .univ]
  simp

Goal state after:
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 : 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
a : β
⊢ ∀ (n : ℕ), Measurable fun c ↦ (F n) (a, c)

pp: case h_mono
α : 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
a : β
⊢ Monotone fun n c ↦ (F n) (a, c)

Tactic:
· exact fun n => (F n).measurable.comp measurable_prodMk_left

Goal state after:
case h_mono
α : 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
a : β
⊢ Monotone fun n c ↦ (F n) (a, c)
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 : 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
⊢ ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a =
    ∫⁻ (x : β), ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂η (a, x) ∂κ a

Tactic:
lintegral_compProd

Goal state after:
α : 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
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), AEMeasurable.mk f hf (b, c) ∂η (a, b) ∂κ a =
    ∫⁻ (x : β), ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂η (a, x) ∂κ a

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)
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case pos.hfi
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ Integrable (fun a ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

pp: case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ 0 ≤ᵐ[μ.restrict s] fun a ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
· exact hf.integrableOn.div_const _

Goal state after:
case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ 0 ≤ᵐ[μ.restrict s] fun a ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ