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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ IsPretransitive (↥G) α

Tactic:
apply IsPretransitive.of_partition (s := s)

Goal state after:
case hs
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b

case hs'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b

case hM
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ stabilizer (↥G) s ≠ ⊤
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock (↥G) B
inst✝ : IsPreprimitive ↥(stabilizer (↥G) B) ↑B
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Subtype.val ⁻¹' B = Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (⟨g', hg'⟩ • B) B
⊢ ⟨g', hg'⟩ • B ⊆ Bᶜ

Tactic:
exact Disjoint.subset_compl_right h

Goal state after:
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 α
⊢ 1 < sᶜ.ncard

Tactic:
exact lt_of_le_of_lt h0.nonempty.ncard_pos hs

Goal state after:
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
⊢ IsTrivialBlock B

Tactic:
IsTrivialBlock,

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
⊢ B.Subsingleton ∨ B = univ
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
⊢ Function.Injective fun s ↦ (↑s.toMonoidHom).toFun

Tactic:
by
    intro ⟨_, _⟩ ⟨_, _⟩ h
    congr
    exact DFunLike.coe_injective h

Goal state after:
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.Section
g₁ g₂ : G
⊢ (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂ ∈ S.inl.range

Tactic:
by
  simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
    mul_assoc, inv_mul_cancel]

Goal state after:
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
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
n : N
hn : S.inl n = (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e
⊢ S.inl (Function.invFun (⇑S'.inl) (S'.inl n)) = S.inl n

Tactic:
Function.leftInverse_invFun S'.inl_injective

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
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
n : N
hn : S.inl n = (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e
⊢ S.inl n = S.inl n
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
s✝ t : ↑(powersetCard α n)
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
g : G
s : ↑(powersetCard α n)
a✝ : α
⊢ a✝ ∈ ↑((compl hm) (g • s)) ↔ a✝ ∈ ↑(id g • (compl hm) s)

Tactic:
simp [← inv_smul_mem_iff]

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
y : α
hy : y ∈ (↑g.support)ᶜ
⊢ ⟨g, hg⟩ • y = y

Tactic:
simpa only [Set.mem_compl_iff, Finset.mem_coe, notMem_support] using! hy

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
⊢ G = ⊤

Tactic:
rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α < 3
⊢ G = ⊤

case inr
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
⊢ G = ⊤
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
u : ℤˣ
a : ↥(toSubgroup A B u)
⊢ ↑((toSubgroupEquiv φ (-u)) ((toSubgroupEquiv φ u) a)) = ↑a

Tactic:
rcases Int.units_eq_one_or u with rfl | rfl
  · simp [toSubgroup]
  · simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe]
    exact φ.apply_symm_apply a

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
⊢ (unitsSMulGroup φ d u g).2 = (⋯.equiv g).2

Tactic:
by
  rcases Int.units_eq_one_or u with rfl | rfl <;> rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
i : M
hi : Irreducible i
u m' : M
hu : IsUnit (f u)
hm' : Irreducible m'
ha0 : u * m' ≠ 0
ha : Irreducible (f (u * m')) → ∃ u_1 m'_1, IsUnit (f u_1) ∧ Irreducible m'_1 ∧ u * m' = u_1 * m'_1
hai : Irreducible (f (u * m')) ∧ IsUnit (f i)
⊢ IsUnit (f (u * i))

Tactic:
by simpa using hu.mul hai.2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∃ g, g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

Tactic:
by
  constructor
  · -- empty case
    intro h
    obtain ⟨g, hg⟩ := h
    constructor
    · rw [← hg, Equiv.Perm.sum_cycleType]
      exact (Equiv.Perm.support g).card_le_univ
    · intro a
      rw [← hg]
      exact Equiv.Perm.two_le_of_mem_cycleType
  · rintro ⟨hc, h2c⟩
    have hc' : m.toList.sum ≤ Fintype.card α := by
      simp only [Multiset.sum_toList]
      exact hc
    obtain ⟨p, hp_length, hp_nodup, hp_disj⟩ := List.exists_pw_disjoint_with_card hc'
    use List.prod (List.map (fun l => List.formPerm l) p)
    have hp2 : ∀ x ∈ p, 2 ≤ x.length := by
      intro x hx
      apply h2c x.length
      rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
      exact ⟨x, hx, rfl⟩
    rw [Equiv.Perm.cycleType_eq _ rfl]
    · -- lengths
      rw [← Multiset.coe_toList m]
      apply congr_arg
      rw [List.map_map]; rw [← hp_length]
      apply List.map_congr_left
      intro x hx; simp only [Function.comp_apply]
      rw [List.support_formPerm_of_nodup x (hp_nodup x hx)]
      · -- length
        rw [List.toFinset_card_of_nodup (hp_nodup x hx)]
      · -- length >= 1
        grind
    · -- cycles
      simpa using fun a b ↦ List.isCycle_formPerm (hp_nodup a b) (hp2 a b)
    · -- disjoint
      rw [List.pairwise_map]
      apply List.Pairwise.imp_of_mem _ hp_disj
      intro a b ha hb hab
      rw [List.formPerm_disjoint_iff (hp_nodup a ha) (hp_nodup b hb) (hp2 a ha) (hp2 b hb)]
      exact hab

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

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

Tactic:
← notMem_support

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∉ g.support
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d).support
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : 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
H : ↑τ c = c
d : ↥g.cycleFactorsFinset
hd : ↑τ d ≠ d
⊢ ↑d x = x

Tactic:
← notMem_support

Goal state after:
case pos
α : 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
H : ↑τ c = c
d : ↥g.cycleFactorsFinset
hd : ↑τ d ≠ d
⊢ x ∉ (↑d).support
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 G ^ ∑ i ∈ Finset.range n, Nat.card G ^ i) ^ Nat.card G * Nat.card G =
    Nat.card G ^ (Nat.card G * ∑ i ∈ Finset.range n, Nat.card G ^ i + 1)

Tactic:
pow_succ,

Goal state after:
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 G ^ ∑ i ∈ Finset.range n, Nat.card G ^ i) ^ Nat.card G * Nat.card G =
    Nat.card G ^ (Nat.card G * ∑ i ∈ Finset.range n, Nat.card G ^ i) * Nat.card G
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
this : sign c = 1
⊢ c.IsCycle

Tactic:
mem_cycleFactorsFinset_iff

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c.IsCycle ∧ ∀ a ∈ c.support, c a = g a
this : sign c = 1
⊢ c.IsCycle
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩

Tactic:
by
  let := H.fintypeQuotientOfFiniteIndex
  let ϕ : H →* H :=
    { toFun := fun h =>
        ⟨g.unop⁻¹ * h * g.unop,
          hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩
      map_one' := by rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
      map_mul' := fun h₁ h₂ => by
        simp only [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left] }
  refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm
  simp only [ϕ, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc,
    MonoidHom.id_apply, toPerm_symm_apply, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
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' : x ∉ Function.fixedPoints ⇑g
⊢ ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯) (↑((u, v).2 ⟨g.cycleOf x, hx⟩) x) =
    ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
← notMem_support

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' : x ∉ Function.fixedPoints ⇑g
⊢ ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∉
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((noncommPiCoprod ⋯) (u, v).2) x = x

Tactic:
← notMem_support

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ x ∉ ((noncommPiCoprod ⋯) (u, v).2).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g x : Perm α
hx : x ∈ g.cycleFactorsFinset
⊢ Fintype.card ↥(zpowers x) = (Finset.card ∘ support) x

Tactic:
rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ (↑⟨c, hc⟩).IsCycle

Tactic:
mem_cycleFactorsFinset_iff

Goal state after:
case e'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc✝ : c ∈ g.cycleFactorsFinset
hc : c.IsCycle ∧ ∀ a ∈ c.support, c a = g a
a✝ : ⟨c, hc✝⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc✝⟩ ^ x) k = ↑(uv ⟨c, hc✝⟩)
⊢ (↑⟨c, hc✝⟩).IsCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s)
⊢ (↑k).support ⊆ s

Tactic:
exact (mem_range_ofSubtype_iff s k).mp (Subgroup.map_le_range _ _ hk)

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

Goal state before:
pp: case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a 1 ^ (k + 1) = a ↑(k + 1)

Tactic:
pow_succ,

Goal state after:
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a 1 ^ k * a 1 = a ↑(k + 1)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ orderOf (a 1) = 2 * n

Tactic:
rcases eq_zero_or_neZero n with rfl | hn

Goal state after:
case inl
⊢ orderOf (a 1) = 2 * 0

case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw : w.fstIdx ≠ some i
hgr : g ∉ (φ i).range
⊢ cons g w hmw hgr = (of i) g • w

Tactic:
by
  apply ext_smul i
  simp only [cons, Word.cons_eq_smul, MonoidHom.apply_ofInjective_symm,
    equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv, mul_smul, inv_smul_smul, summand_smul_def,
    equivPair, rcons, Word.equivPair_symm, Word.rcons_eq_smul, Equiv.coe_fn_mk,
    Word.equivPair_tail_eq_inv_smul, Equiv.coe_fn_symm_mk, smul_inv_smul]

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

Goal state before:
pp: n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

Tactic:
rcases eq_zero_or_neZero n with rfl | hn

Goal state after:
case inl
⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4

case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ Group.IsSolvable G

Tactic:
by
  rw [Group.isSolvable_iff_commutator_lt]
  intro H h
  rw [← H.nontrivial_iff_ne_bot] at h
  rw [← H.range_subtype, MonoidHom.range_eq_map, ← Subgroup.map_commutator,
    Subgroup.map_subtype_lt_map_subtype]
  exact commutator_lt H

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
this : IsCyclic ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
exact isCyclic_of_surjective f f.surjective

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i ↦ Classical.decEq (G i)
a₁✝ a₂✝ : H
h : ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₁✝ = ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
exact eq_of_smul_eq_smul (fun w : NormalWord d =>
    by simp_all [funext_iff, base_smul_eq_smul])

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ (base φ).range ≤ (of j).range

Tactic:
by rw [← of_comp_eq_base j]
          rintro _ ⟨h, rfl⟩
          exact MonoidHom.mem_range.2 ⟨φ j h, rfl⟩

Goal state after:
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.normalizer ↑P ≤ Subgroup.centralizer (⇑(Subgroup.normalizer ↑P).subtype '' ↑↑Q)
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

Tactic:
rwa [← Subgroup.coe_map, P.coe_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
⊢ κ = Kernel.sum fun n ↦ if n = 0 then κ else 0

Tactic:
ext a s hs
      rw [Kernel.sum_apply' _ _ hs]
      have : (fun i => ((ite (i = 0) κ 0) a) s) = fun i => ite (i = 0) (κ a s) 0 := by
        ext1 i; split_ifs <;> rfl
      rw [this, tsum_ite_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ((η.restrict hs) b) t ∂κ a = (((η ∘ₖ κ).restrict hs) a) t

Tactic:
restrict_apply' _ _ _ ht,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (η b) (t ∩ s) ∂κ a = ((η ∘ₖ κ) a) (t ∩ s)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
⊢ ⇑(const β μ ∘ₖ κ) = fun a ↦ (κ a) Set.univ • μ

Tactic:
by
  ext _ _ hs
  simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
    smul_eq_mul, mul_comm]

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

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

Tactic:
rw [comp_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsMarkovKernel η
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
⊢ IsProbabilityMeasure ((κ a).bind ⇑η)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:

Tactic:
∫⁻ a, (Prod.mk a ⁻¹' s).indicator 1 a ∂μ
  _ = ∫⁻ a, (Function.diag ⁻¹' s).indicator 1 a ∂μ := rfl
  _ = μ (Function.diag ⁻¹' s) := by
    rw [lintegral_indicator_one]
    exact (measurable_id.prod measurable_id) hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Kernel.id (f a✝¹)) s✝ = (Measure.dirac (f a✝¹)) s✝

Tactic:
Kernel.id_apply

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Measure.dirac (f a✝¹)) s✝ = (Measure.dirac (f a✝¹)) s✝
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a =
    ((κ ⊗ₖ prodMkLeft X (Kernel.id ×ₖ η)) a) (Prod.snd ⁻¹' s)

Tactic:
compProd_apply

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a =
    ∫⁻ (b : Y), ((prodMkLeft X (Kernel.id ×ₖ η)) (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a

case hs
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)