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

Goal state before:
pp: α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝¹ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
this : Subsingleton ↑(powersetCard α n)
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 0 ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ derivedSeries G (n + 1) = ⊤

Tactic:
derivedSeries_succ,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ ⁅derivedSeries G n, derivedSeries G n⁆ = ⊤
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
⊢ Group (HNNExtension.con G A B φ).Quotient

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
Knorm : K.Normal
⊢ H.Normal

Tactic:
| step H K h_le hSubn hN Knorm =>

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
u' : ℤˣ
⊢ ∀ (g : G), (u', g) ∈ (u, w.head) :: w.toList → g ∈ d.set u'

Tactic:
g'

Goal state after:
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
u' : ℤˣ
g' : G
⊢ (u', g') ∈ (u, w.head) :: w.toList → g' ∈ d.set u'
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
⊢ m₁ = m₂

Tactic:
let ⟨a⟩ := ‹Nonempty Λ›

Goal state after:
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
⊢ m₁ = m₂
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite PUnit.{u + 1}

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

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

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Group G
⊢ Group PUnit.{u + 1}

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case succ
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n✝ : ℕ
inst✝ : Group G
n : ℕ
ih : Group (IteratedWreathProduct G n)
⊢ Group (IteratedWreathProduct G n ≀ᵣ G)

Tactic:
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
⊢ Mul (con φ).Quotient

Tactic:
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 (con φ).Quotient

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case intro
ι : 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
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
⊢ f.comp (base φ) = g.comp (base φ)

Tactic:
ext
      rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]

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 φ
w₁ w₂ : NormalWord d
hhead : w₁.head = w₂.head
hlist : w₁.toList = w₂.toList
⊢ w₁ = w₂

Tactic:
rcases w₁ with ⟨⟨_, _, _⟩, _, _⟩

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 φ
w₂ : NormalWord d
head✝ : H
toList✝ : List ((i : ι) × G i)
ne_one✝ : ∀ l ∈ toList✝, l.snd ≠ 1
chain_ne✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) toList✝
normalized✝ :
  ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList → g ∈ d.set i
hhead :
  { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.head =
    w₂.head
hlist :
  { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.toList =
    w₂.toList
⊢ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ } = w₂
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 ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
⊢ Nat.card ↥N * N.index = N.index * Nat.card ↥N

Tactic:
mul_comm

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 ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
⊢ N.index * Nat.card ↥N = N.index * Nat.card ↥N
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 ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
h7 : Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G
h8 : (Nat.card ↥N).Coprime (Nat.card ↥(map K.subtype H))
⊢ ∃ H, N.IsComplement' H

Tactic:
exact ⟨H.map K.subtype, isComplement'_of_coprime h7 h8⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
that : (↑k).cycleType.card = #c.support
⊢ (card ∘ support) c = #c.support

Tactic:
by simp only [Function.comp_apply]

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
g : Perm α
hg0 : g ∈ alternatingGroup α
n : ℕ
hg : orderOf g ∣ 2 ^ n
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
by
  rw [mem_alternatingGroup, sign_of_cycleType] at hg0
  have h1 : g.cycleType.sum ≤ 4 := by
    rw [sum_cycleType, ← hα4, Nat.card_eq_fintype_card]
    exact g.support.card_le_univ
  have h2 : ∀ k ∈ g.cycleType, k = 2 := by
    intro k hk
    have hk4 := (Multiset.le_sum_of_mem hk).trans h1
    have hk1 := one_lt_of_mem_cycleType hk
    interval_cases k
    · rfl
    · rw [← lcm_cycleType, Multiset.lcm_dvd] at hg
      exact Nat.prime_eq_prime_of_dvd_pow Nat.prime_three Nat.prime_two (hg 3 hk)
    · contrapose! hg0
      obtain ⟨t, ht⟩ := Multiset.exists_cons_of_mem hk
      rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff,
        Multiset.sum_eq_zero_iff, ← Multiset.eq_replicate_card] at h1
      have h : 0 ∉ g.cycleType := Nat.not_succ_lt_self ∘ one_lt_of_mem_cycleType
      replace h : t = 0 := by simpa [h1 ▸ ht, Multiset.mem_replicate] using h
      simp [ht, h, Units.ext_iff]
  rw [← Multiset.eq_replicate_card] at h2
  rw [h2, Multiset.sum_replicate, smul_eq_mul, ← Nat.le_div_iff_mul_le two_pos] at h1
  interval_cases g.cycleType.card <;> simp [h2, Units.ext_iff] at hg0 ⊢

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
S : Sylow 2 ↥(alternatingGroup α)
⊢ Nat.card ↥↑S = 4

Tactic:
Sylow.card_eq_multiplicity,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 2 ^ (Nat.card ↥(alternatingGroup α)).factorization 2 = 4
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑({1} ∪ {g | (↑g).cycleType = {2, 2}}) ≤ Fintype.card ↑↑S

Tactic:
simp_rw [← Nat.card_eq_fintype_card]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Nat.card ↑({1} ∪ {g | (↑g).cycleType = {2, 2}}) ≤ Nat.card ↑↑S
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
inst✝¹ : DecidableEq α
inst✝ : (s : Set α) → DecidablePred fun x ↦ x ∈ s
s : ↑(Set.powersetCard α 2)
this : IsMulCommutative (Perm ↥↑s)
⊢ IsMulCommutative ↥ofSubtype.range

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : ↑(Set.powersetCard α 3)
this : IsMulCommutative ↥(alternatingGroup ↥↑s)
⊢ IsMulCommutative ↥(ofSubtype ↑s).range

Tactic:
infer_instance

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 : ↑(Set.powersetCard α 4)
this : IsMulCommutative ↥(kleinFour ↥↑s)
⊢ IsMulCommutative ↥(Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))

Tactic:
infer_instance

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

Goal state before:
pp: 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
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime ↑p)
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
x✝ : CommGroup G := { toGroup := inst✝⁴, mul_comm := ⋯ }
⊢ IsCyclic G

Tactic:
exact IsCyclic.of_exponent_eq_card (exponent_eq_card G)

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

Goal state before:
pp: case ind.inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⊥

Tactic:
infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : Abelianization.of.ker ≤ Subgroup.center ↥(commutator ↥H)
x✝ : CommGroup ↥(commutator ↥H) := commGroupOfCyclicCenterQuotient Abelianization.of h
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
infer_instance

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
η : Kernel α β
a : α
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrProbabilityMeasure 0

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
η : Kernel α β
h : IsZeroOrMarkovKernel 0
⊢ IsFiniteKernel 0

Tactic:
infer_instance

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 α β
f : α → β
hf : Measurable f
a : α
⊢ IsProbabilityMeasure (Measure.dirac (f a))

Tactic:
infer_instance

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
h✝ : ¬n = 0
⊢ IsFiniteKernel 0

Tactic:
infer_instance

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 α β
⊢ IsMarkovKernel (deterministic id ⋯)

Tactic:
infer_instance

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 α β
⊢ IsMarkovKernel (deterministic Function.diag ⋯)

Tactic:
infer_instance

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
h : ∀ i ∈ ∅, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel 0

Tactic:
infer_instance

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 α β
⊢ IsMarkovKernel (deterministic (fun x ↦ PUnit.unit) ⋯)

Tactic:
infer_instance

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 α β
⊢ IsMarkovKernel (deterministic Prod.swap ⋯)

Tactic:
infer_instance

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)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
x : (i : ι) → β i
i : ι
⊢ k • 0 = 0

Tactic:
by simp_rw [smul_zero]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
hμβ : IsZeroOrProbabilityMeasure 0
⊢ IsZeroOrMarkovKernel 0

Tactic:
infer_instance

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
hμβ : IsZeroOrProbabilityMeasure μβ
h : IsProbabilityMeasure μβ
⊢ IsZeroOrMarkovKernel (const α μβ)

Tactic:
infer_instance

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)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
hk : ∀ (i : ι), IsSMulRegular (β i) k
x : (i : ι) → β i
i : ι
⊢ k • 0 = 0

Tactic:
by simp_rw [smul_zero]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
⊢ swap α α ∘ₖ copy α = copy α

Tactic:
ext a s hs
  rw [comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _), swap_apply' _ hs,
    Measure.dirac_apply' _ hs]
  congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ μ s✝ * (κ x✝) Set.univ = (κ x✝) Set.univ * μ s✝

Tactic:
mul_comm

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

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure μ

Tactic:
infer_instance

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

Goal state before:
pp: case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ν

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsZeroOrMarkovKernel 0
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsZeroOrMarkovKernel η
inst✝ : IsZeroOrMarkovKernel 0
h✝ : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel 0

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
h✝ : IsMarkovKernel κ
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst✝ : IsZeroOrMarkovKernel η
h✝¹ : IsMarkovKernel κ
h✝ : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (Kernel.sum fun i ↦ Kernel.sum fun i_1 ↦ η.seq i ∘ₖ κ.seq i_1)

Tactic:
infer_instance

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

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

Tactic:
simp only [SimpleFunc.coe_add, Pi.add_apply]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ⇑g₁) (support ⇑g₂)
hm₁ : Measurable fun a ↦ ∫⁻ (b : β), g₁ (a, b) ∂κ a
hm₂ : Measurable fun a ↦ ∫⁻ (b : β), g₂ (a, b) ∂κ a
⊢ Measurable fun a ↦ ∫⁻ (b : β), g₁ (a, b) + g₂ (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 : α × γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∫⁻ (x_1 : β), (η x.2) (Prod.mk x_1 ⁻¹' Set.univ) ∂κ x.1 = (κ x.1) Set.univ * (η x.2) Set.univ

Tactic:
mul_comm

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 : α × γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∫⁻ (x_1 : β), (η x.2) (Prod.mk x_1 ⁻¹' Set.univ) ∂κ x.1 = (η x.2) Set.univ * (κ x.1) Set.univ
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 : α × γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ((κ ∥ₖ η) x) Set.univ = (κ x.1) Set.univ * (η x.2) Set.univ

Tactic:
rw [parallelComp_apply, Measure.prod_apply .univ, mul_comm]

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 : α × γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∫⁻ (x_1 : β), (η x.2) (Prod.mk x_1 ⁻¹' Set.univ) ∂κ x.1 = (η x.2) Set.univ * (κ x.1) Set.univ