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

Goal state before:
pp: case succ
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
ih : (pi Set.univ Ss).lowerCentralSeries n = pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n
⊢ ⁅(pi Set.univ Ss).lowerCentralSeries n, pi Set.univ Ss⁆ = pi Set.univ fun i ↦ ⁅(Ss i).lowerCentralSeries n, Ss i⁆

Tactic:
ih,

Goal state after:
case succ
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
ih : (pi Set.univ Ss).lowerCentralSeries n = pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n
⊢ ⁅pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n, pi Set.univ Ss⁆ =
    pi Set.univ fun i ↦ ⁅(Ss i).lowerCentralSeries n, Ss i⁆
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
B✝ : Set X
B : IsBlock G B✝
⊢ B✝.Subsingleton

Tactic:
exact Set.subsingleton_of_subsingleton

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
hst : s = t
x✝¹ x✝ : ↥(ofFixingSubgroup M s)
hxy : (ofFixingSubgroup_of_eq M hst) x✝¹ = (ofFixingSubgroup_of_eq M hst) x✝
⊢ x✝¹ = x✝

Tactic:
by simpa [← SetLike.coe_eq_coe] using hxy

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

Goal state before:
pp: case inr.inl
α : 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 : 1 < sᶜ.encard
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
obtain ⟨g, hg, hg'⟩ := this sᶜ h1c

Goal state after:
case inr.inl
α : 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 : 1 < sᶜ.encard
g : Perm α
hg : g.IsSwap
hg' : g ∈ stabilizer (Perm α) sᶜ
⊢ ∃ g, g.IsSwap ∧ g ∈ G
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : g ∈ stabilizer (Perm α) s
hg3 : g.IsThreeCycle
⊢ ⟨g, ⋯⟩ ∈ ↑G ∧ (alternatingGroup α).subtype ⟨g, ⋯⟩ = g

Tactic:
simpa only [SetLike.mem_coe, Subgroup.subtype_apply, and_true] using hG hg

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

Goal state before:
pp: n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
⊢ IsMultiplyPreprimitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1

Tactic:
rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]

Goal state after:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
⊢ IsMultiplyPreprimitive G α (Nat.succ 1)

case hn
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
⊢ 1 ≤ 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ B = univ

Tactic:
suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    grind

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ sᶜ ⊆ B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ sᶜ ⊆ B

Tactic:
have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    apply compl_ne_univ.mpr h0.nonempty -- `sᶜ ≠ univ`
    apply hsc.eq_univ_of_card_lt
    grind

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
⊢ sᶜ ⊆ B
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
⊢ toPerm g = 1

Tactic:
ext1 s

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 : fixedPoints G ↑(powersetCard α n) = univ
s : ↑(powersetCard α n)
⊢ (toPerm g) s = 1 s
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: 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₁ s₂ s₃ : S.Splitting
h₂ : S.IsConj s₂ s₃
n₁ : N
hn₁ : ⇑s₁ = fun g ↦ S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
⊢ S.IsConj s₁ s₃

Tactic:
obtain ⟨n₂, hn₂⟩ := h₂

Goal state after:
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₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g ↦ S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g ↦ S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ S.IsConj s₁ s₃
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✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑a.2 * a.1 * (↑c.2 * b.1) ≤ ↑a.2 * a.1 * (↑b.2 * c.1)
⊢ ↑c.2 * b.1 ≤ ↑b.2 * c.1

Tactic:
exact le_of_mul_le_mul_left' hab

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✝ c✝ : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 * mk b.1 b.2 ≤ mk a.1 a.2 * mk c.1 c.2
⊢ mk b.1 b.2 ≤ mk c.1 c.2

Tactic:
simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ a.1] at hab ⊢
      exact le_of_mul_le_mul_left' hab

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x✝¹ x✝ : α × ↥s
⊢ ↑x✝.2 * x✝¹.1 ≤ ↑x✝¹.2 * x✝.1 ∨ ↑x✝¹.2 * x✝.1 ≤ ↑x✝.2 * x✝¹.1

Tactic:
exact le_total _ _

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right.h
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
⊢ u.Disjoint v

Tactic:
exact huv

Goal state after:
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:
ih,

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) • w = cons g u w h1 h2
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
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
ih :
  ∀ (chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l),
    ∃ w',
      ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := chain } ∧
        List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := chain }.toList ∧
          ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := chain }.toList.head?,
            w'.head ∈ toSubgroup A B (-u)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain } ∧
      List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)

Tactic:
rcases ih (List.isChain_cons.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩
    clear ih
    refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩
    · rw [prod_smul, hw'1]
      simp [ReducedWord.prod]
    · have : ¬ Cancels a.1 (a.2 • w') := by
        simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some_iff,
          Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists]
        intro hS x hx
        have hx' := congr_arg (Option.map Prod.fst) hx
        rw [← List.head?_map, hw'2, List.head?_map, Option.map_some] at hx'
        have : w'.head ∈ toSubgroup A B a.fst := by
          simpa using hw'3 _ hx'
        rw [mul_mem_cancel_right this] at hS
        have : a.fst = -a.fst := by
          have hl : l ≠ [] := by rintro rfl; simp_all
          have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
            (List.head?_eq_some_head _) hS
          rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
        simp at this
      simp [mul_smul, of_smul_eq_smul, t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2]

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
a b c : D ≀ᵣ Q
⊢ a * b * c = a * (b * c)

Tactic:
ext <;> simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case succ
G : Type u
n✝ : ℕ
inst✝ : Finite G
n : ℕ
h : Nat.card (IteratedWreathProduct G n) = Nat.card G ^ ∑ i ∈ Finset.range n, Nat.card G ^ i
⊢ Nat.card (IteratedWreathProduct G (n + 1)) = Nat.card G ^ ∑ i ∈ Finset.range (n + 1), Nat.card G ^ i

Tactic:
rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1

Tactic:
simp_rw [residuallyFinite_def, Subgroup.eq_bot_iff_forall, Subgroup.mem_iInf,
    FiniteIndexNormalSubgroup.mem_toSubgroup_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
c : ↥g.cycleFactorsFinset
x✝¹ : c ∈ U
d : ↥g.cycleFactorsFinset
x✝ : d ∈ U
h : c ≠ d
⊢ (fun i j ↦ (↑(v i)).Disjoint ↑(v j)) c d

Tactic:
obtain ⟨m, hm⟩ := (v c).prop
    obtain ⟨n, hn⟩ := (v d).prop
    simp only [← hm, ← hn]
    apply Disjoint.zpow_disjoint_zpow
    apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop
    exact Subtype.coe_ne_coe.mpr h

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τ⟩
⊢ sign ↑k = -1

Tactic:
have hk_cT : k.val.cycleType = Multiset.replicate k.val.cycleType.card 2 := by
    rw [Multiset.eq_replicate_card, ← pow_prime_eq_one_iff, ← Subgroup.coe_pow,
      ← Subgroup.coe_one, Subtype.coe_inj, hk, ← map_pow]
    convert! MonoidHom.map_one _
    rw [← Subtype.coe_inj]
    apply Equiv.swap_mul_self

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
τ : 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
⊢ sign ↑k = -1
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 ↥N
inst✝ : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
| map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N

Tactic:
conv =>

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 ↥N
inst✝ : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
| map N.subtype ⊤
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
hG : Nat.card G = n
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
⊢ ∃ H, N.IsComplement' H

Tactic:
revert G
  induction n using Nat.strongRecOn with | ind n ih => ?_
  rintro G _ _ rfl N _ hN
  refine not_forall_not.mp fun h3 => ?_
  have := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3
  exact not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN)

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

Goal state before:
pp: case inr
α : 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 α)
hk22 : (↑k).cycleType = (↑g).cycleType
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
← Equiv.Perm.isConj_iff_cycleType_eq,

Goal state after:
case inr
α : 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 α)
hk22 : IsConj ↑k ↑g
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | DihedralGroup.r j => a j
      | DihedralGroup.sr j => xa j)
    fun x ↦
    match x with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j

Tactic:
rintro (k | k) <;> rfl

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

Goal state before:
pp: n : ℕ
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | DihedralGroup.r j => a j
      | DihedralGroup.sr j => xa j)
    fun x ↦
    match x with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j

Tactic:
rintro (k | k) <;> rfl

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)
⊢ IsMulCommutative ↥(Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))

Tactic:
have : IsMulCommutative (kleinFour s) :=
      (kleinFour_isKleinFour (by simp)).isMulCommutative
    infer_instance

Goal state after:
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 φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw✝ : w.fstIdx ≠ some i
_hgn✝ : g ∈ d.set i
hgr✝ : g ∉ (φ i).range
_hw1✝ : w.head = 1
ih : w.prod • empty = w
⊢ (of i) g • w.prod • empty = cons g w hmw✝ hgr✝

Tactic:
ih,

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 φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw✝ : w.fstIdx ≠ some i
_hgn✝ : g ∈ d.set i
hgr✝ : g ∉ (φ i).range
_hw1✝ : w.head = 1
ih : w.prod • empty = w
⊢ (of i) g • w = cons g w hmw✝ hgr✝
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingDist 0 x = hammingNorm x

Tactic:
rw [hammingDist_comm, hammingDist_zero_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((κ.comapRight hf) a) t = (κ a) (f '' t)

Tactic:
rw [comapRight_apply,
    Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ ((swap α α) (a, a)) s = (Measure.dirac (a, a)) s

Tactic:
swap_apply' _ hs,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ s.indicator 1 (a, a).swap = (Measure.dirac (a, a)) s
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✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
b : Bool
⊢ ((boolKernel μ ν) b) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

Tactic:
cases b

Goal state after:
case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) false) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) true) Set.univ ≤ max (μ Set.univ) (ν Set.univ)
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✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
b : Bool
⊢ IsProbabilityMeasure ((boolKernel μ ν) b)

Tactic:
cases b

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

case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ((boolKernel μ ν) true)