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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
x✝ : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
this : ∃ x ∈ s, y = f x
⊢ φ g • y = y

Tactic:
by
        obtain ⟨x, hx, rfl⟩ := this
        rwa [← map_smulₛₗ, hg]

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

Goal state before:
pp: case h.inr.inr
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 α
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
have : Set.Nontrivial sᶜ := by
      rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
    -- get a, b ∈ sᶜ, a ≠ b
    obtain ⟨a, ha : a ∈ sᶜ, b, hb : b ∈ sᶜ, hab⟩ := this
    -- apply Rudio to get g ∈ G such that a ∈ g • sᶜ, b ∉ g • sᶜ
    obtain ⟨g, hga, hgb⟩ := exists_mem_smul_and_notMem_smul (G := G)
      sᶜ.toFinite (Set.nonempty_of_mem ha)
      (by simpa [Set.nonempty_iff_ne_empty] using hs_nonempty)
      hab
    let t := s ∩ g • s
    have ha : a ∉ s ∪ g • s := by
      simp only [Set.smul_set_compl, Set.mem_compl_iff] at hga ha
      simp [ha, hga]
    have htm : t.ncard = t.ncard - 1 + 1 := by
      apply (Nat.sub_eq_iff_eq_add ?_).mp rfl
      rw [Nat.one_le_iff_ne_zero, ← Nat.pos_iff_ne_zero, Set.ncard_pos]
      apply Set.nonempty_inter_of_le_ncard_add_ncard
      · rw [Set.ncard_smul_set, ← two_mul, hsn]; exact hn2
      · exact fun h ↦ ha (by rw [h]; trivial)
    have hmn : t.ncard - 1 < n := by
      rw [Nat.lt_iff_add_one_le, ← htm, Nat.le_iff_lt_add_one, ← hsn]
      apply Set.ncard_lt_ncard _
      refine ⟨Set.inter_subset_left, fun h ↦ hb ?_⟩
      suffices s = g • s by
        rw [this]
        simpa only [Set.smul_set_compl, Set.mem_compl_iff, Set.not_notMem] using hgb
      apply Set.eq_of_subset_of_ncard_le _ _ (g • s).toFinite
      · exact subset_trans h Set.inter_subset_right
      · rw [Set.ncard_smul_set]
    have htm' : t.ncard - 1 + 2 < Nat.card α := lt_trans (Nat.add_lt_add_right hmn 2) hsn'
    have hsgs_ne_top : s ∪ g • s ≠ ⊤ := fun h ↦ ha (h ▸ Set.mem_univ a)
    suffices IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) →
      IsMultiplyPretransitive G α 2 by
      refine ⟨this, fun hs_prim ↦ ?_⟩
      apply (hrec _ hmn hG htm htm').2
      exact IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
          hs_prim hsgs_ne_top
    intro hs_trans
    apply (hrec _ hmn hG htm htm').1
    exact IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs_trans hsgs_ne_top

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬s.ncard + sᶜ.ncard = s.ncard + s.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
Nat.add_left_cancel_iff

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) 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.Splitting
x✝ : N ⋊[s.conjAct] G
n : N
g : G
⊢ (fun e ↦ ⟨Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩)
      ((fun x ↦
          match x with
          | ⟨n, g⟩ => S.inl n * s g)
        ⟨n, g⟩) =
    ⟨n, g⟩

Tactic:
by
    simp only [map_mul, rightHom_inl, rightHom_splitting, one_mul, mul_inv_cancel_right,
      Function.leftInverse_invFun S.inl_injective n]

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

Goal state before:
pp: case inr.hprim
α : 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 α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ Nat.Prime (Nat.card ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ))

Tactic:
convert! Nat.prime_three

Goal state after:
α : 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 α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ Nat.card ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ) = 3
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsPerfect ↥⊤ ↔ IsPerfect G

Tactic:
isPerfect_def,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ _root_.commutator ↥⊤ = ⊤ ↔ IsPerfect G
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ _root_.commutator ↥⊤ = ⊤ ↔ IsPerfect G

Tactic:
isPerfect_def,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ _root_.commutator ↥⊤ = ⊤ ↔ _root_.commutator G = ⊤
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
n : ℕ
S : AddSubgroup M
inst✝¹ : Free ℤ ↥(toIntSubmodule S)
inst✝ : Module.Finite ℤ ↥(toIntSubmodule S)
⊢ (map (nsmulAddMonoidHom n) S).relIndex S = n ^ finrank ℤ ↥S

Tactic:
by
  simpa only [relIndex, addSubgroupOf_map_nsmulAddMonoidHom_eq_range]
    using! index_range_nsmul S.toIntSubmodule n

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

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

Tactic:
rw [mul_assoc, of_mul_t]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
hH : H ≠ K
⊢ H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
simpa [*] using HK.lt_of_ne hH

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

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

pp: case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a

Tactic:
· simp [toSubgroup]

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a
Module: Mathlib.GroupTheory.HNNExtension

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

Tactic:
· simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe]
    exact φ.apply_symm_apply a

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ H.IsSubnormal

Tactic:
obtain rfl | ⟨K, HK, Ksn, h⟩ := h

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
⊢ ⊤.IsSubnormal

case inr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∃ n f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤

Tactic:
use n + 1, fun | 0 => H | n + 1 => f n, ?_, ?_

Goal state after:
case right
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ (match 0 with
      | 0 => H
      | n.succ => f n) =
      H ∧
    (match n + 1 with
      | 0 => H
      | n.succ => f n) =
      ⊤

case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ Monotone fun x ↦
    match x with
    | 0 => H
    | n.succ => f n

case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
⊢ ∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o

Tactic:
let klift (n : ℕ) (hn : n < Fintype.card α) : Fin (Fintype.card α) :=
    (⟨n, hn⟩ : Fin (Fintype.card α))
  let klift' (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) :
    List (Fin (Fintype.card α)) := List.pmap klift l hl
  have hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α := by
    intro l hl n hn
    apply lt_of_lt_of_le _ hc
    rw [← mem_mem_ranges_iff_lt_sum]
    exact ⟨l, hl, hn⟩
  let l := (ranges c).pmap klift' hc'_lt
  have hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges),
    (klift' a (hc'_lt a ha)).map Fin.valEmbedding = a := by
    intro a ha
    conv_rhs => rw [← List.map_id a]
    rw [List.map_pmap]
    simp [klift, Fin.valEmbedding_apply, List.pmap_eq_map, List.map_id']
  use l.map (List.map (Fintype.equivFin α).symm)
  constructor
  · -- length
    rw [← ranges_length c]
    simp only [l, klift', map_pmap, length_pmap,
      pmap_eq_map]
  constructor
  · -- nodup
    intro s
    rw [mem_map]
    rintro ⟨t, ht, rfl⟩
    apply Nodup.map (Equiv.injective _)
    obtain ⟨u, hu, rfl⟩ := mem_pmap.mp ht
    apply Nodup.of_map
    rw [hl u hu]
    exact ranges_nodup hu
  · -- pairwise disjoint
    refine Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_
    -- List.Pairwise List.disjoint l
    apply Pairwise.pmap (List.ranges_disjoint c)
    intro u hu v hv huv
    apply disjoint_pmap
    · intro a a' ha ha' h
      simpa only [klift, Fin.mk_eq_mk] using h
    exact huv

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

Goal state before:
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:
List.pairwise_map

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 (fun a b ↦ a.formPerm.Disjoint b.formPerm) p
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
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ w',
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
hw1 : ¬w.head = 1
w' : NormalWord d
hw' :
  ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := w.toList, chain := ⋯ } ∧
    List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ }.toList ∧
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ }.toList.head?,
        w'.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ (w.head • w').toReducedWord = ReducedWord.prod φ w ∧
    List.map Prod.fst (w.head • w').toList = List.map Prod.fst w.toList ∧
      ∀ u ∈ Option.map Prod.fst w.toList.head?, (w.head • w').head⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
simpa [ReducedWord.prod, mul_assoc] using hw'

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✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
⊢ Nat.card (Fin n → G) = p ^ n

Tactic:
by rw [Nat.card_fun, Nat.card_fin, hG]

Goal state after:
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 τ
  rw [mem_range_toPermHom_iff, mem_range_toPermHom'_iff]

Goal state after:
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ᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H := { toFun := fun h ↦ ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩

Tactic:
refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H := { toFun := fun h ↦ ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
x : G ⧸ H
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ =
    ϕ
      ((MonoidHom.id ↥H)
        ⟨(↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)))⁻¹ * ↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)),
          ⋯⟩)
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : h • Quotient.mk'' α = Quotient.mk'' α
⊢ h ^ H.index = (diff (MonoidHom.id ↥H) α (op ↑h⁻¹ • α))⁻¹

Tactic:
smul_diff',

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : h • Quotient.mk'' α = Quotient.mk'' α
⊢ h ^ H.index = (diff (MonoidHom.id ↥H) α α * h⁻¹ ^ H.index)⁻¹
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case H.inl
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
g : CoprodI G
⊢ motive ↑(inl g)

Tactic:
induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ Finite G

Tactic:
apply Nat.finite_of_card_ne_zero

Goal state after:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card G ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ↑S = Subgroup.closure ↑?m.28

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Sylow 2 ↥(alternatingGroup α)

Tactic:
exact S.closure_eq.symm

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

Goal state before:
pp: case e'_2.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {1}
⊢ g = 1

Tactic:
simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'

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

Goal state before:
pp: case hx
⊢ orderOf ?x = Nat.card (QuaternionGroup 1)

pp: case x
⊢ QuaternionGroup 1

Tactic:
· rw [Nat.card_eq_fintype_card, card, mul_one]
    exact orderOf_xa 0

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
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
⊢ CoprodI.of ((φ i) (cons g w hmw hgr).head) • (cons g w hmw hgr).toWord =
    CoprodI.of ((φ i) ((of i) g • w).head) • ((of i) g • w).toWord

Tactic:
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.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 : ↑Q ≤ Subgroup.center ↥(Subgroup.normalizer ↑P)
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

Tactic:
← SetLike.coe_subset_coe,

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 : ↑↑Q ⊆ ↑(Subgroup.center ↥(Subgroup.normalizer ↑P))
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
C : ℝ≥0∞
hC : C < ∞
hle : ∀ (a : α), (κ a) Set.univ ≤ C
⊢ κ.bound < ∞

Tactic:
refine lt_of_le_of_lt ?_ hC

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
C : ℝ≥0∞
hC : C < ∞
hle : ∀ (a : α), (κ a) Set.univ ≤ C
⊢ κ.bound ≤ C
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y < 1 ↔ x = y

Tactic:
Nat.lt_one_iff,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 ↔ x = y
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
a : α
⊢ (copy α) a = Measure.dirac (a, a)

Tactic:
simp [copy, deterministic_apply]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
a : α
ha : a ∈ sᶜ
b : α
hb : b ∉ s
⊢ IsProbabilityMeasure ((piecewise s_meas (const α (κ a)) κ) b)

Tactic:
· simpa [hb, piecewise] using! hs _ hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (x : β), (η b.2) (Prod.mk x ⁻¹' s) ∂κ b.1

Tactic:
refine Measurable.lintegral_kernel_prod_right'
        (f := fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s)) (κ := prodMkRight γ κ) ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((deterministic f hf ∘ₖ κ) a) s = ((κ.map f) a) s

Tactic:
simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
    lintegral_indicator_const_comp hf hs, one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
⊢ deterministic g hg ∘ₖ deterministic f hf = deterministic (g ∘ f) ⋯

Tactic:
ext; simp [comp_deterministic_eq_comap, comap_apply, deterministic_apply]

Goal state after: