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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
⊢ ↑(Fintype.card ↑(Set.range fun g ↦ g • B)) ≤ (orbit H B).ncard

Tactic:
← Set.toFinset_card,

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
⊢ ↑(Set.range fun g ↦ g • B).toFinset.card ≤ (orbit H B).ncard
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
⊢ Nat.card α ≤ 3

Tactic:
← not_lt

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
⊢ ¬3 < Nat.card α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ k ∈ (ofSubtype s).range ↔ (↑k).support ⊆ s

Tactic:
range_ofSubtype,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ k ∈ Perm.ofSubtype.range.subgroupOf (alternatingGroup α) ↔ (↑k).support ⊆ s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
φ : Perm α ≃* Perm α
a✝ : Nontrivial α
⊢ (comap φ.toMonoidHom (alternatingGroup α)).index = 2

Tactic:
index_comap_of_surjective _ (Equiv.surjective _),

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
φ : Perm α ≃* Perm α
a✝ : Nontrivial α
⊢ (alternatingGroup α).index = 2
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
⊢ ⟨↑m, ⋯⟩ ∈ fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)

Tactic:
let hm := m.prop
      simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm
      rintro ⟨⟨x, hx⟩, hx'⟩
      simp only [Set.mem_preimage] at hx'
      simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]
      exact hm.right ⟨x, hx'⟩

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

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
⊢ t.ncard ≠ 0

Tactic:
apply Set.ncard_ne_zero_of_mem (a := a) _ ht

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := ⋯
ht : t.Finite
⊢ a ∈ t
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case h'
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
⊢ Nat.card α ≤ s.ncard + s.ncard

Tactic:
← two_mul,

Goal state after:
case h'
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
⊢ Nat.card α ≤ 2 * s.ncard
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
⊢ swap a b * swap a c ∈ alternatingGroup α

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
k : ↥(alternatingGroup α)
hk✝ : k ∈ stabilizer (↥(alternatingGroup α)) sᶜ
hk : k ∈ stabilizer (↥(alternatingGroup α)) s
⊢ ⟨k, ⋯⟩ ∈ stabilizer (↥G) sᶜ

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
⊢ sᶜ ≠ ∅

Tactic:
by aesop

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : sᶜ.ncard * 2 ≤ Nat.card α
⊢ False

Tactic:
← not_lt

Goal state after:
case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ B ≠ sᶜ

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
⊢ IsCoatom (stabilizer ↥(alternatingGroup α) {a})

Tactic:
stabilizer_singleton

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) a)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ (Nat.card α).factorial ≤ 2 * Nat.card ↥G

Tactic:
apply le_trans (Nat.factorial_le hα4)

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ Nat.factorial 3 ≤ 2 * Nat.card ↥G
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
u : ℤˣ
w : NormalWord d
this✝ : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem : ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u
this : w.head ∈ toSubgroup A B u
⊢ u = u'

Tactic:
have := h this x

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
u : ℤˣ
w : NormalWord d
this✝¹ : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem : ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u
this✝ : w.head ∈ toSubgroup A B u
this : ¬w.toList.head? = some (-u, x)
⊢ u = u'
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
a : α
⊢ φ a = i ↔ f ((Equiv.refl α) a) = ↑i

Tactic:
rw [refl_apply, ← Subtype.coe_inj]

Goal state after:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
a : α
⊢ ↑(φ a) = ↑i ↔ f a = ↑i
Module: Mathlib.GroupTheory.RegularWreathProduct

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

Tactic:
Nat.card_fun

Goal state after:
D : Type u_1
Q : Type u_2
inst✝ : Finite Q
⊢ Nat.card D ^ Nat.card Q * Nat.card Q = Nat.card D ^ Nat.card Q * Nat.card Q
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even ({n}.sum + {n}.card) then #{g | g.cycleType = {n}} else #∅) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
simp only [Multiset.sum_singleton, Multiset.card_singleton, Finset.card_empty]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even (n + 1) then #{g | g.cycleType = {n}} else 0) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_1.right
ι : 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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ⟨i, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ w.toList.tail ∨
    w.toList.head? = some ⟨i, ((Word.equivPair i) w).head⟩ ∨ ¬w.fstIdx = some i ∧ ((Word.equivPair i) w).head = 1

Tactic:
rw [Word.equivPair_head]
      dsimp
      split_ifs with hep
      · rcases hep with ⟨hnil, rfl⟩
        rw [head?_eq_some_head hnil]
        simp_all
      · push Not at hep
        by_cases hw : w.toList = []
        · simp [hw, Word.fstIdx]
        · simp [head?_eq_some_head hw, Word.fstIdx, hep hw]

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
H : ⟨c, hc⟩ ≠ ⟨d, hd⟩
⊢ ∑ x ∈ {⟨c, hc⟩, ⟨d, hd⟩}, #(↑x).support = #c.support * 2

Tactic:
rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),
      Finset.sum_singleton, hm, mul_two]

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 : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i✝ : ι
p : Pair d i✝
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i✝).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
i : ι
g : G i
hg : ⟨i, g⟩ ∈ w.toList
⊢ g ∈ d.set i

Tactic:
by
        dsimp [w] at hg
        rw [Word.equivPair_symm, Word.mem_rcons_iff] at hg
        rcases hg with hg | ⟨_, rfl, rfl⟩
        · exact p.normalized _ _ hg
        · simp

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 : ι) → 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⟩ ∈ p.tail.toList
⊢ g ∈ d.set j

Tactic:
dsimp only [p] 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) (CoprodI.of ((φ i) w.head) • 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
⊢ (kleinFour α).Characteristic

Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  have _ := subsingleton_two_sylow hα4
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
  exact Sylow.characteristic_of_subsingleton _

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 α)
hg : (↑g).cycleType = {2, 2}
c : Perm α
hc : c * ↑k * c⁻¹ = ↑g
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc

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 α)
hg : (↑g).cycleType = {2, 2}
c : Perm α
hc : (MulAut.conjNormal c) k = g
⊢ g ∈ commutator ↥(alternatingGroup α)
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
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
d : Transversal φ
⊢ w = Word.empty

Tactic:
rcases hw.exists_normalWord_prod_eq d with ⟨w', hw'prod, hw'map⟩

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
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ w = Word.empty
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: 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
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Tactic:
have : IsCyclic Q :=
    isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe P.le_normalizer).symm.surjective

Goal state after:
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
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator 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
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P → ¬p ∣ Nat.card ↥(commutator G)

Tactic:
refine fun hP h ↦ P.not_dvd_index (h.trans ?_)

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
hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ (↑P).index
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
⊢ ↑P ≤ commutator G → ¬p ∣ (commutator G).index

Tactic:
refine fun hP h ↦ P.not_dvd_index (h.trans ?_)

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
hP : ↑P ≤ commutator G
h : p ∣ (commutator G).index
⊢ (commutator G).index ∣ (↑P).index
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ({ toFun := fun a ↦ Measure.dirac (f a), measurable' := ⋯ } a) s = s.indicator (fun x ↦ 1) (f a)

Tactic:
change Measure.dirac (f a) s = s.indicator 1 (f a)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ (Measure.dirac (f a)) s = s.indicator 1 (f a)
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι) (m : ℕ), (((κs i).seq m) a) s = ∑' (n : ℕ), (fun im ↦ (((κs im.1).seq im.2) a) s) (e n)

Tactic:
e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s),

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι) (m : ℕ), (((κs i).seq m) a) s = ∑' (b : ι × ℕ), (((κs b.1).seq b.2) 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 α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (piecewise hs κ η) a = (Kernel.sum fun n ↦ piecewise hs (κ.seq n) (η.seq n)) a

Tactic:
simp_rw [sum_apply, Kernel.piecewise_apply]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (if a ∈ s then κ a else η a) = Measure.sum fun n ↦ if a ∈ s then (κ.seq n) a else (η.seq n) a
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h✝ : IsSFiniteKernel κ
h : IsSFiniteKernel η
⊢ IsSFiniteKernel (Kernel.sum fun i ↦ κ.seq i ∥ₖ Kernel.sum η.seq)

Tactic:
parallelComp_sum_right

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h✝ : IsSFiniteKernel κ
h : IsSFiniteKernel η
⊢ IsSFiniteKernel (Kernel.sum fun i ↦ Kernel.sum fun i_1 ↦ κ.seq i ∥ₖ η.seq i_1)
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 γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ (Kernel.id.map f).map g = deterministic (g ∘ f) ⋯

Tactic:
← map_comp_right _ hf hg,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ Kernel.id.map (g ∘ f) = deterministic (g ∘ f) ⋯