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

Goal state before:
pp: case hstep
⊢ ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
· intro G _ _ ih H hH
    have hch : center G ≤ H := Subgroup.center_le_normalizer H |>.trans (le_of_eq hH)
    have hkh : (mk' (center G)).ker ≤ H := by simpa using hch
    have hsur : Function.Surjective (mk' (center G)) := Quot.mk_surjective
    let H' := H.map (mk' (center G))
    have hH' : normalizer H' = H' := by
      apply comap_injective hsur
      rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
      exact hH
    apply map_injective_of_ker_le (mk' (center G)) hkh le_top
    exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur))

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ False

Tactic:
obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg

Goal state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g₁ g₂ : G
hB : IsBlock G ∅
hg : g₁ • ∅ ⊆ g₂ • ∅
hg' : g₁ • ∅ ≠ g₂ • ∅
⊢ False
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ Cardinal.toENat (Cardinal.mk ↥(ofStabilizer G a)) + 1 = Cardinal.toENat (Cardinal.mk ↑{a} + Cardinal.mk ↑{a}ᶜ)

Tactic:
map_add,

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ Cardinal.toENat (Cardinal.mk ↥(ofStabilizer G a)) + 1 =
    Cardinal.toENat (Cardinal.mk ↑{a}) + Cardinal.toENat (Cardinal.mk ↑{a}ᶜ)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ).IsThreeCycle
hτ : (↑τ).IsThreeCycle
⊢ IsConj σ τ

Tactic:
simp only [Nat.card_eq_fintype_card] at h5

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ).IsThreeCycle
hτ : (↑τ).IsThreeCycle
h5 : 5 ≤ card α
⊢ IsConj σ τ
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
this : IsPreprimitive ↥(fixingSubgroup M (s ∪ t')) ↥(ofFixingSubgroup M (s ∪ t'))
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))

Tactic:
apply IsPreprimitive.of_surjective map_ofFixingSubgroupUnion_bijective.surjective

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)

Tactic:
apply H.isPreprimitive_ofFixingSubgroup
      simp [← hs, t, hf.injective.injOn.encard_image]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
⊢ IsTrivialBlock B

Tactic:
by
  rcases le_or_gt (Nat.card α) 2 with h2 | h2
  · exact isTrivialBlock_of_card_le_two h2 B
  rcases le_or_gt (Nat.card α) 3 with h3 | h4
  · replace h3 : Nat.card α = 3 := le_antisymm h3 h2
    have : IsPretransitive (alternatingGroup α) α := isPretransitive_of_three_le_card α h3.ge
    have : IsPreprimitive (alternatingGroup α) α := IsPreprimitive.of_prime_card (h3 ▸ prime_three)
    exact this.isTrivialBlock_of_isBlock hB
  -- IsTrivialBlock hB, for 4 ≤ Nat.card α
  suffices IsPreprimitive (alternatingGroup α) α by
    apply IsPreprimitive.isTrivialBlock_of_isBlock hB
  apply isPreprimitive_of_is_two_pretransitive
  let := isMultiplyPretransitive α
  apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)
  rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_of_lt h2)]

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

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ 1 ≤ s.encard

Tactic:
one_le_encard_iff_nonempty,

Goal state after:
case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ s.Nonempty
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ 1 ≤ sᶜ.encard

Tactic:
one_le_encard_iff_nonempty,

Goal state after:
case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ sᶜ.Nonempty
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
this : ∃ g, g ∉ stabilizer (↥(alternatingGroup α)) s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

Tactic:
contrapose! this; simp [this]

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ ⇑S.rightHom ∘ ⇑equiv.symm = ⇑S'.rightHom

Tactic:
rw [MulEquiv.comp_symm_eq, ← equiv.rightHom_comm]

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂
⊢ S.inl n = (σ (g₁ * g₂))⁻¹ * (σ g₁ * σ g₂)

Tactic:
← mul_assoc,

Goal state after:
case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂
⊢ S.inl n = (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂
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
⊢ finrank ℤ ↥A = finrank ℤ M

Tactic:
refine le_antisymm A.toIntSubmodule.finrank_le ?_

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
⊢ finrank ℤ M ≤ finrank ℤ ↥A
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ n i * (f ↑(x (n i)).2 * f ↑(∏ x_1 ∈ univ.erase i, (x (n x_1)).2)) =
    f ((fun i ↦ (x (n i)).1 * ↑(∏ j ∈ univ.erase i, (x (n j)).2)) i)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ n i * f ↑(x (n i)).2 * f ↑(∏ x_1 ∈ univ.erase i, (x (n x_1)).2) =
    f ((fun i ↦ (x (n i)).1 * ↑(∏ j ∈ univ.erase i, (x (n j)).2)) i)
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a b : Localization s
⊢ a ≤ b → b ≤ a → a = b

Tactic:
by
    induction a using Localization.rec
    on_goal 1 =>
      induction b using Localization.rec
      · simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
        exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩
    all_goals rfl

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
b : α
hb : b ∈ T
⊢ ¬closure S ≤ stabilizer G T

Tactic:
obtain ⟨σ, rfl⟩ := subset hb

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun m ↦ m • a) σ ∈ T
⊢ ¬closure S ≤ stabilizer G T
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (of g * (t ^ ↑u * ReducedWord.prod φ w.toReducedWord)) • empty = cons g u w h1 h2

Tactic:
← mul_assoc,

Goal state after:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (of g * t ^ ↑u * ReducedWord.prod φ w.toReducedWord) • empty = cons g u w h1 h2
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
⊢ Equiv.swap a c ∈ M

Tactic:
obtain rfl | hab' := eq_or_ne a b

Goal state after:
case inl
α : Type u_2
inst✝² : DecidableEq α
a c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a a ∈ M
hbc : Equiv.swap a c ∈ M
⊢ Equiv.swap a c ∈ M

case inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
⊢ Equiv.swap a c ∈ M
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 : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
| (g ^ j * g) x

Tactic:
← zpow_add_one

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
| (g ^ (j + 1)) x
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
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 : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left (m₁.right * (m₁.right⁻¹ * q)) • a = m₂.left (m₂.right * (m₁.right⁻¹ * q)) • a
⊢ m₁.left q = m₂.left q

Tactic:
← (h a b).2

Goal state after:
case left
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 : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left (m₁.right * (m₁.right⁻¹ * q)) • a = m₂.left (m₁.right * (m₁.right⁻¹ * q)) • a
⊢ m₁.left q = m₂.left q
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
rw [notMem_support.mp hx, eq_comm, ← notMem_support,
      ofPermHomFun_apply_mem_support_cycle_iff]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ x ∉ (↑c).support
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
⊢ (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index

Tactic:
have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])

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
⊢ (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∀ ⦃x : Perm α⦄, x ∈ Finset.univ → ¬x.cycleType = m) ↔ ¬∃ g, g.cycleType = m

Tactic:
not_exists

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∀ ⦃x : Perm α⦄, x ∈ Finset.univ → ¬x.cycleType = m) ↔ ∀ (x : Perm α), ¬x.cycleType = m
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).IsThreeCycle
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
by
  rw [commutator_eq_closure]
  apply Subgroup.subset_closure
  exact hg.mem_commutatorSet_alternatingGroup h5

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ #{i | x i ≠ y i} = #{i | y i ≠ x i}

Tactic:
ne_comm

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

Goal state before:
pp: case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
ht : t ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)

Tactic:
simp only [Set.mem_image2, Set.mem_ofPred_eq] at ht

Goal state after:
case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
ht : ∃ a, MeasurableSet a ∧ ∃ b, MeasurableSet b ∧ a ×ˢ b = t
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
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:
by
    refine ⟨fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n), fun n ↦ inferInstance, ?_⟩
    ext b
    rw [Kernel.sum_apply]
    cases b <;> simp [sum_sfiniteSeq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun x ↦ ∫⁻ (y : γ), f (x, y) ∂η (a, x)

Tactic:
by
  change
    Measurable
      ((fun x => ∫⁻ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))
  -- Porting note: specified `κ`, `f`.
  refine (Measurable.lintegral_kernel_prod_right' (κ := η)
    (f := (fun u ↦ f (u.fst.snd, u.snd))) ?_).comp measurable_prodMk_left
  fun_prop

Goal state after:
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:
by
  rw [parallelComp_apply, Measure.prod_apply .univ, mul_comm]
  simp

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

Goal state before:
pp: case pos.inl
α : 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 δ
f✝ : β → γ
g : γ → α
f : β → γ
hf : Measurable f
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (Kernel.map 0 f)

Tactic:
simp only [map_zero]

Goal state after:
case pos.inl
α : 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 δ
f✝ : β → γ
g : γ → α
f : β → γ
hf : Measurable f
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0
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 α β
f : β → γ
g : β → δ
hg : Measurable g
⊢ (κ.map fun x ↦ (f x, g x)).fst = κ.map f

Tactic:
by
  by_cases hf : Measurable f
  · ext x s hs
    rw [fst_apply' _ _ hs, map_apply' _ (hf.prod hg) _, map_apply' _ hf _ hs]
    · simp only [Set.preimage, Set.mem_ofPred]
    · exact measurable_fst hs
  · have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hf; exact hf.fst
    simp [map_of_not_measurable _ hf, map_of_not_measurable _ this]

Goal state after:
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
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂η (a, b) ∂κ a

Tactic:
let g := Function.curry f

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 : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂η (a, b) ∂κ a
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

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

Tactic:
← mul_assoc,

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : 𝓧
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ (ν univ)⁻¹ * ν univ * μ.rnDeriv ν x = μ.rnDeriv ν x
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 γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum fun m ↦ κ.seq n ⊗ₖ η.seq m) a) s = ∑' (n : ℕ) (m : ℕ), ((κ.seq n ⊗ₖ η.seq m) a) s

Tactic:
sum_apply' _ _ hs

Goal state after: