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

Goal state before:
pp: case h1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty

Tactic:
simpa [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq] using ne_of_lt hn

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑a * t⁻¹ = t⁻¹ * of ↑(φ a)

Tactic:
equiv_eq_conj

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑a * t⁻¹ = t⁻¹ * (t * of ↑a * t⁻¹)
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst✝¹ : (i : ι) → CommMonoid (M i)
inst✝ : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
⊢ ∃ x, z * Pi.map f ↑x.2 = Pi.map f x.1

Tactic:
by
    choose x hx using fun i ↦ (hf i).surj
    exact ⟨⟨fun i ↦ (x i (z i)).1, ⟨_, fun i _ ↦ (x i (z i)).2.2⟩⟩, funext fun i ↦ hx i (z i)⟩

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
u : ℤˣ
hu : ¬u = 1
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))

Tactic:
by
    convert! φ.symm <;>
    cases Int.units_eq_one_or u <;> simp_all

Goal state after:
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₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
⊢ ↑c₂ * a₁ < ↑a₂ * c₁ ↔ ↑d₂ * b₁ < ↑b₂ * d₁

Tactic:
obtain ⟨e, he⟩ := r_iff_exists.1 hab
        obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
        simp only [mul_right_inj] at he hf
        rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]

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
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h
    else
      let g' := unitsSMulGroup φ d 1 (↑g • w).head;
      cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Tactic:
dif_neg (mt this.1 hcan),

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (let g' := unitsSMulGroup φ d 1 (↑g • w).head;
    cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ ∀ σ ∈ List.map (fun l ↦ l.formPerm) p, σ.IsCycle

pp: case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise Disjoint (List.map (fun l ↦ l.formPerm) p)

Tactic:
· -- cycles
      simpa using fun a b ↦ List.isCycle_formPerm (hp_nodup a b) (hp2 a b)

Goal state after:
case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise Disjoint (List.map (fun l ↦ l.formPerm) p)
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
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g✝ : G
hg✝ : g✝ ∈ closure S
g g' : G
x✝¹ : g ∈ closure S
x✝ : g' ∈ closure S
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ

Tactic:
← compl_inter,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g✝ : G
hg✝ : g✝ ∈ closure S
g g' : G
x✝¹ : g ∈ closure S
x✝ : g' ∈ closure S
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g ∩ fixedBy α g')ᶜ
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
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : g ∈ closure S
⊢ (fixedBy α g)ᶜ.Finite

Tactic:
refine closure_induction h (by simp) (fun g g' _ _ hg hg' ↦ (hg.union hg').subset ?_)
      (by simp) hg
    simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]

Goal state after:
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 : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑τ c)) ∈ (↑(↑τ c)).support

Tactic:
rw [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]
      apply mem_support_self

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✝
G : Type u_3
inst✝ : Group G
n : ℕ
⊢ IteratedWreathProduct G (n + 1) →* Equiv.Perm (Fin (n + 1) → G)

Tactic:
let _ := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)

Goal state after:
D : Type u_1
Q : Type u_2
inst✝³ : Group D
inst✝² : Group Q
G✝ : Type u
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u_3
inst✝ : Group G
n : ℕ
x✝ : MulAction (IteratedWreathProduct G n) (Fin n → G) := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)
⊢ IteratedWreathProduct G (n + 1) →* Equiv.Perm (Fin (n + 1) → G)
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
n : ℕ
⊢ Function.Injective ⇑(iteratedWreathToPermHom G (n + 1))

Tactic:
let _ := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)

Goal state after:
G : Type u_3
inst✝ : Group G
n : ℕ
x✝ : MulAction (IteratedWreathProduct G n) (Fin n → G) := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)
⊢ Function.Injective ⇑(iteratedWreathToPermHom G (n + 1))
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (toPermHom g).range = range_toPermHom' g

Tactic:
ext τ

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ τ ∈ (toPermHom g).range ↔ τ ∈ range_toPermHom' g
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
obtain ⟨a, ha1, ha2⟩ := mem_support_of_mem_noncommProd_support hx'

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha1 : a ∈ Finset.univ.erase ⟨g.cycleOf x, hx⟩
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
⊢ x ∈ Function.fixedPoints ⇑g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ #(if Even (m.sum + m.card) then {g | g.cycleType = m} else ∅) *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0

Tactic:
apply_ite Finset.card,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then #{g | g.cycleType = m} else #∅) *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ #(if Even (m.sum + m.card) then {g | g.cycleType = m} else ∅) = 0

Tactic:
apply_ite Finset.card,

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ (if Even (m.sum + m.card) then #{g | g.cycleType = m} else #∅) = 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
⊢ ∀ x ∈ g.cycleFactorsFinset, ∀ y ∈ g.cycleFactorsFinset, #x.support = #y.support → x = y

Tactic:
by_contra! ⟨c, hc, d, hd, hm, hm'⟩

Goal state after:
α : 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
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!

Tactic:
rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]
  rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
  convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
  · ext h
    simp only [Set.mem_ofPred_eq, ConjAct.mem_orbit_conjAct, isConj_comm]
  · rw [ConjAct.card, Fintype.card_perm]

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
this✝ : Nontrivial ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ IsMulCommutative ↥N

Tactic:
exact
    ⟨⟨fun g h => ((eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left
      (step6 h1 h2 h3).bot_lt_center.ne') (mem_top h)).comm g).symm⟩⟩

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

Goal state before:
pp: case «3»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : 3 ≤ 4
hk1 : 1 < 3
⊢ 3 = 2

Tactic:
rw [← lcm_cycleType, Multiset.lcm_dvd] at hg

Goal state after:
case «3»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : ∀ b ∈ g.cycleType, b ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : 3 ≤ 4
hk1 : 1 < 3
⊢ 3 = 2
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 : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
w : NormalWord d
p : Word.Pair G i := (Word.equivPair i) (CoprodI.of ((φ i) w.head) • w.toWord)
j : ι
g : G j
hg :
  ⟨j, g⟩ ∈
    (have __src := (Word.equivPair i) w.toWord;
        { head := (φ i) w.head * ((Word.equivPair i) w.toWord).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.toList
⊢ g ∈ d.set j

Tactic:
dsimp at hg

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
w : NormalWord d
p : Word.Pair G i := (Word.equivPair i) (CoprodI.of ((φ i) w.head) • w.toWord)
j : ι
g : G j
hg : ⟨j, g⟩ ∈ ((Word.equivPair i) w.toWord).tail.toList
⊢ g ∈ d.set j
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this✝ : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
c : Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
this : ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
⊢ (MulAut.conjNormal c) k ∈ Subgroup.map (MulEquiv.toMonoidHom fc) ⁅⊤, ⊤⁆

Tactic:
refine Subgroup.mem_map_of_mem _ hk

Goal state after:
Module: Mathlib.InformationTheory.Coding.UniquelyDecodable

Goal state before:
pp: α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L // ∀ (x : List α), x ∈ L → x ∈ S }
⊢ (fun L ↦ (↑L).flatten) L₁ = (fun L ↦ (↑L).flatten) L₂ → L₁ = L₂

Tactic:
hflat

Goal state after:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L // ∀ (x : List α), x ∈ L → x ∈ S }
hflat : (fun L ↦ (↑L).flatten) L₁ = (fun L ↦ (↑L).flatten) L₂
⊢ L₁ = L₂
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ ⁅commutator ↥H, commutator ↥H⁆ ≤ Subgroup.centralizer ↑(commutator ↥H)

Tactic:
Subgroup.le_centralizer_iff

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h : commutator ↥⊤ ≤ (Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆).subgroupOf ⊤
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
← Subgroup.map_subtype_le_map_subtype,

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h :
  Subgroup.map ⊤.subtype (commutator ↥⊤) ≤
    Subgroup.map ⊤.subtype ((Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆).subgroupOf ⊤)
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
replace hG k : ϕ k = 1 ∨ IsUnit (ϕ k - 1) := by
    obtain ⟨n, hn⟩ := hG.exists_card_eq
    exact ZMod.eq_one_or_isUnit_sub_one hn (ϕ k)
      (hGK.symm.coprime_dvd_left ((orderOf_map_dvd ϕ k).trans (orderOf_dvd_natCard k)))

Goal state after:
case neg
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ⊤ ≤ Subgroup.centralizer ↑↑Q
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

Tactic:
← Subgroup.map_subtype_le_map_subtype,

Goal state after:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h :
  Subgroup.map (Subgroup.normalizer ↑P).subtype ⊤ ≤
    Subgroup.map (Subgroup.normalizer ↑P).subtype (Subgroup.centralizer ↑↑Q)
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : (↑P).subgroupOf (Subgroup.normalizer ↑P) ≤ commutator ↥(Subgroup.normalizer ↑P)
⊢ ↑P ≤ commutator G

Tactic:
← Subgroup.map_subtype_le_map_subtype,

Goal state after:
case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h :
  Subgroup.map (Subgroup.normalizer ↑P).subtype ((↑P).subgroupOf (Subgroup.normalizer ↑P)) ≤
    Subgroup.map (Subgroup.normalizer ↑P).subtype (commutator ↥(Subgroup.normalizer ↑P))
⊢ ↑P ≤ commutator G
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η : Kernel α β
inst✝ : Countable ι
κ : ι → Kernel α β
⊢ Measurable fun a ↦ Measure.sum fun n ↦ (κ n) a

Tactic:
refine Measure.measurable_of_measurable_coe _ fun s hs => ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η : Kernel α β
inst✝ : Countable ι
κ : ι → Kernel α β
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (Measure.sum fun n ↦ (κ n) b) s
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
⊢ Measurable fun a ↦ Measure.dirac (f a)

Tactic:
refine Measure.measurable_of_measurable_coe _ fun s hs => ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (Measure.dirac (f 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)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
x : (i : ι) → β i
i : ι
⊢ k • 0 = 0

Tactic:
simp_rw [smul_zero]

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:
simp_rw [smul_zero]

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
⊢ concatFn w₁ = concatFn w₂ → w₁ = w₂

Tactic:
hflat

Goal state after:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
⊢ w₁ = w₂
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ (concatFn w).length ∈ Finset.Icc r (r * S.sup List.length)

Tactic:
rw [concatFn_length, Finset.mem_Icc]

Goal state after:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ r ≤ ∑ i, (↑(w i)).length ∧ ∑ i, (↑(w i)).length ≤ r * S.sup List.length
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ discard β ∘ₖ κ = discard α

Tactic:
ext; simp [comp_discard']

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, κ a = 0
⊢ μ ⊗ₘ κ = 0

Tactic:
· rw [← compProd_zero_right μ]
    exact compProd_congr h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = 0 ↔ ∀ᵐ (a : α) ∂μ, κ a = 0

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simp_rw [← measure_univ_eq_zero]
    refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_
    rw [← setLIntegral_univ, ← compProd_apply_prod .univ .univ, h]
    simp
  · rw [← compProd_zero_right μ]
    exact compProd_congr h

Goal state after: