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

Goal state before:
pp: case inl
⊢ orderOf (r 1) = 0

Tactic:
orderOf_eq_zero_iff'

Goal state after:
case inl
⊢ ∀ (n : ℕ), 0 < n → r 1 ^ n ≠ 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
rw [lift, Equiv.coe_fn_mk, Con.lift_range, FreeMonoid.mrange_lift,
    range_sigma_eq_iUnion_range, Submonoid.closure_iUnion]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ ⨆ i, Submonoid.closure (range fun b ↦ (f ⟨i, b⟩.fst) ⟨i, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂

Tactic:
rcases cs.exists_isReduced w₁ with ⟨ω₁, hω₁, rfl⟩
  rcases cs.exists_isReduced w₂ with ⟨ω₂, hω₂, rfl⟩
  have := cs.length_wordProd_le (ω₁ ++ ω₂)
  simpa [hω₁.eq, hω₂.eq, wordProd_append] using this

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1

Tactic:
rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]

Goal state after:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
m m' : M
s s' : ℕ+
⊢ mk m s = mk m' s' ↔ ↑s' • m = ↑s • m'

Tactic:
aesop (add simp [mk_eq_mk, nsmul_right_inj])

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
⊢ h * (Quotient.out (mk H K g) * k) = g

Tactic:
rw [← mul_assoc, ← T]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
⊢ x = y

Tactic:
have heq₂ : x ^ (2 * n) = y ^ (2 * n) := by simp_rw [mul_comm, pow_mul, heq]

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
⊢ x = y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ H.subtype.range.lowerCentralSeries n = H.lowerCentralSeries n

Tactic:
subtype_range

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ H.lowerCentralSeries n = H.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
rw [nilpotencyClass_def]
  refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
  · intro n hn
    exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩
  · rintro n ⟨H, ⟨hH, hn⟩⟩
    rw [← top_le_iff, ← hn]
    exact ascending_central_series_le_upper H hH n

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
let I' : Subgroup (G' × H') := (P.prod Q).range

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
i : η
⊢ ⊤.lowerCentralSeries (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)) = ⊥

Tactic:
rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]

Goal state after:
case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
i : η
⊢ nilpotencyClass (Gs i) ≤ Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hbase
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
H : Subgroup G
a✝ : normalizer ↑H = H
⊢ H = ⊤

Tactic:
exact @Subsingleton.elim _ Unique.instSubsingleton _ _

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
⊢ normalizer ↑H = H → H = ⊤

Tactic:
hH

Goal state after:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
⊢ H = ⊤
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
apply Or.intro_right; simp only [hB]; apply Set.preimage_univ

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
⊢ IsBlock G (B₁ ∩ B₂)

Tactic:
simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢
  rintro g₁ g₂ ⟨a, ha₁, ha₂⟩
  rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ H.Normal

Tactic:
hH

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ ⊤.Normal
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
have hag : ∀ g : G, a ∈ g • B' → B' ≤ g • B' := by
    intro g hg x hx
    -- a = g • b; b ∈ B'; a ∈ k • B → b ∈ k • B
    simp only [B', Set.mem_iInter, Set.mem_smul_set_iff_inv_smul_mem,
      smul_smul, ← mul_inv_rev] at hg hx ⊢
    exact fun _ ↦ hx _ ∘ hg _

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ (alternatingGroup α).index = 1

Tactic:
Subgroup.index_eq_one

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ alternatingGroup α = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * (g' * g' * c)).IsThreeCycle

Tactic:
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
    exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
⊢ center ↥(alternatingGroup α) = ⊥

Tactic:
eq_bot_iff

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
⊢ center ↥(alternatingGroup α) ≤ ⊥
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
Perm.mem_range_ofSubtype_iff

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ ↑(↑k).support ⊆ {x | x ∈ s} ↔ (↑k).support ⊆ s
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B✝ : Type u_1
inst✝¹⁸ : TopologicalSpace B✝
F✝ : Type u_2
inst✝¹⁷ : NormedAddCommGroup F✝
inst✝¹⁶ : NormedSpace ℝ F✝
E✝ : B✝ → Type u_3
inst✝¹⁵ : TopologicalSpace (TotalSpace F✝ E✝)
inst✝¹⁴ : (x : B✝) → NormedAddCommGroup (E✝ x)
inst✝¹³ : (x : B✝) → InnerProductSpace ℝ (E✝ x)
inst✝¹² : FiberBundle F✝ E✝
inst✝¹¹ : VectorBundle ℝ F✝ E✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
h : v ≠ 0
⊢ ((g.inner b) v) v ≠ 0

Tactic:
exact (g.pos b v h).ne'

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
⊢ ∃ b, b ∈ s

Tactic:
rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
⊢ s ≠ ∅
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := ⋯
x' : Fin (Fintype.card α - 1) ↪ α := ⋯
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (g • x) j

Tactic:
rw [hgk' j hj, hxj]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅Subgroup.upperCentralSeries G 2, _root_.commutator G⁆ = ⊥

Tactic:
commutator_comm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅_root_.commutator G, Subgroup.upperCentralSeries G 2⁆ = ⊥
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))

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

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : M
⊢ f x = 1 → x = 1

Tactic:
simpa using h x 1

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ ↑((g (f a)) ⟨stabilizerEquiv_invFun (fun i ↦ Equiv.symm (g i)) a, ⋯⟩) = a

Tactic:
exact congr_arg Subtype.val ((g <| f a).right_inv _)

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x y : α
⊢ (fixedBy α (swap x y))ᶜ.Finite

Tactic:
exact finite_compl_fixedBy_swap

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Tactic:
obtain ⟨c, hc, m, hm⟩ := hx

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ x ∈ (a.ofPermHom τ).support ↔ x ∈ (↑τ).support.biUnion fun c ↦ (↑c).support

Tactic:
simp only [mem_support, Finset.mem_biUnion, ofPermHom_apply]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x
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 φ
w₁ w₂ : NormalWord d
hhead : w₁.head = w₂.head
hlist : w₁.toList = w₂.toList
⊢ w₁ = w₂

Tactic:
by
  rcases w₁ with ⟨⟨_, _, _⟩, _, _⟩
  rcases w₂ with ⟨⟨_, _, _⟩, _, _⟩
  simp_all

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
h7 : Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G
⊢ (Nat.card ↥N).Coprime (Nat.card ↥(map K.subtype H))

Tactic:
hH

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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
h7 : Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G
⊢ (Nat.card ↥N).Coprime N.index
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ Nat.card ↥(kleinFour α) = 4

Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S, card_two_sylow_of_card_eq_four hα4 S]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ kleinFour α = commutator ↥(alternatingGroup α)

Tactic:
have _ : (kleinFour α).Normal := normal_kleinFour hα4

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ kleinFour α = commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inl
⊢ orderOf (a 1) = 0

Tactic:
orderOf_eq_zero_iff'

Goal state after:
case inl
⊢ ∀ (n : ℕ), 0 < n → QuaternionGroup.a 1 ^ n ≠ 1
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0

Tactic:
apply mt a.inj

Goal state after:
case inl
n : ℕ
h : 0 < n
⊢ ¬↑n = 0
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₂✝
w : NormalWord d
⊢ a₁✝ • w = a₂✝ • w

Tactic:
by simp_all [funext_iff, base_smul_eq_smul]

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)
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
by
      let f := Subgroup.equivMapOfInjective (commutator H) _ H.subtype_injective
      rw [Subgroup.map_subtype_commutator] at f
      exact isCyclic_of_surjective f f.surjective

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ #{i | x i ≠ y i} = #{x_1 | (-x) x_1 + y x_1 ≠ 0}

Tactic:
Pi.neg_apply,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ #{i | x i ≠ y i} = #{x_1 | -x x_1 + y x_1 ≠ 0}
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 β γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ∘ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [comp_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ (Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)) t = (Measure.comap f (Measure.sum fun n ↦ (κ.seq n) a)) t

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

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ∑' (i : ℕ), (Measure.comap f ((κ.seq i) a)) t = ∑' (i : ℕ), ((κ.seq i) a) (f '' t)
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
⊢ Tendsto (fun r ↦ ↑r * ↑maxLen / K ^ r) atTop (nhds 0)

Tactic:
simpa [mul_left_comm, mul_div_assoc] using!
      (tendsto_self_mul_const_pow_of_abs_lt_one hAbs).const_mul (maxLen : ℝ)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = 0

Tactic:
Kernel.compProd_of_not_isSFiniteKernel_right,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ 0 () = 0

case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ ¬IsSFiniteKernel (Kernel.prodMkLeft Unit κ)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable fun x ↦ (f x, g x)
⊢ Measurable f

Tactic:
exact hf.fst

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
⊢ μ s = 0

Tactic:
have h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0 := h h1

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0
⊢ μ s = 0