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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : ¬f b = b
⊢ b = a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : ¬f b = b
⊢ b = a
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : 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
⊢ (¬∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x) ↔ ↑τ c = c

Tactic:
simpa using

Goal state after:
case neg
α : 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
⊢ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
⊢ ∀ {m₁ m₂ : D ≀ᵣ Q},
    (∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right) → m₁ = m₂

Tactic:
intro m₁ m₂ h

Goal state after:
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
⊢ m₁ = m₂
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
this : ReducedWord.prod φ w = ReducedWord.prod φ w'
⊢ w.toList = []

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
this : ReducedWord.prod φ w = ReducedWord.prod φ w'
⊢ w.toList = []
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) → τ ∈ (toPermHom g).range

Tactic:
obtain ⟨a⟩ := Basis.nonempty g
    exact fun hτ ↦ ⟨toCentralizer a ⟨τ, hτ⟩, toPermHom_apply_toCentralizer a ⟨τ, hτ⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
g : G
hg : g ≠ 1
w✝² : Type u
w✝¹ : Group w✝²
w✝ : Finite w✝²
f : G →* w✝²
hf : f g ≠ 1
⊢ g ∉ f.ker

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
g : G
hg : g ≠ 1
w✝² : Type u
w✝¹ : Group w✝²
w✝ : Finite w✝²
f : G →* w✝²
hf : f g ≠ 1
⊢ ¬f g = 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case H.inl.one
ι : 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)
⊢ motive ↑(inl 1)

Tactic:
simpa using

Goal state after:
case H.inl.one
ι : 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)
⊢ motive 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ #{g | (↑g).cycleType = m} =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
    else 0

Tactic:
by
  split_ifs with hm
  · -- m is an even cycle_type
    rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
      Equiv.Perm.card_of_cycleType α m, if_pos hm.1, mul_assoc]
  · -- m does not correspond to a permutation, or to an odd one,
    rw [← Finset.card_map, map_subtype_of_cycleType]
    rw [apply_ite Finset.card, Finset.card_empty]
    split_ifs with hm'
    · rw [Equiv.Perm.card_of_cycleType, if_neg]
      obtain hm | hm := not_and_or.mp hm
      · exact hm
      · contradiction
    · rfl

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_2
ι : 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
this : ((Word.equivPair i) w).head = (φ i) h * ((Word.equivPair i) w).head
⊢ h = 1

Tactic:
simpa using

Goal state after:
case refine_2
ι : 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
this : ((Word.equivPair i) w).head = (φ i) h * ((Word.equivPair i) w).head
⊢ h = 1
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤

Tactic:
have h6 :
    (Nat.card (N.map (QuotientGroup.mk' K))).Coprime (N.map (QuotientGroup.mk' K)).index := by
    have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
    have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
    rw [index_map]
    refine h1.coprime_dvd_left ?_
    rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]
    exact K.card_quotient_dvd_card

Goal state after:
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    #{g | g.cycleType = m}

Tactic:
apply Nat.div_eq_of_eq_mul_left

Goal state after:
case pos.H1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!

case pos.H2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Fintype.card α)! =
    #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ #{g | g.cycleType = {n}} * (n * (card α - n)!) = (card α)!

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ #{g | g.cycleType = {n}} * (n * (card α - n)!) = (card α)!
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
⊢ x ∈ (kerParam g).range ↔ x ∈ Subgroup.centralizer {g}

Tactic:
refine ⟨fun hx ↦ kerParam_range_le_centralizer hx, fun hx ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ x ∈ (kerParam g).range
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
hg0 : 4 ≠ 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
h : 0 ∉ g.cycleType
⊢ t = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
hg0 : 4 ≠ 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
h : 0 ∉ g.cycleType
⊢ t = 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ Subgroup.centralizer {g} ≤ alternatingGroup α ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

Tactic:
rw [SetLike.le_def]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ (∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α) ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
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 α)
k : ↥(alternatingGroup α)
hk : k ∈ ↑S
n : ℕ
hn : orderOf ⟨k, hk⟩ = 2 ^ n
⊢ orderOf ↑k = 2 ^ n

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ ↑S
n : ℕ
hn : orderOf ⟨k, hk⟩ = 2 ^ n
⊢ orderOf k = 2 ^ n
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 using

Goal state after:
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
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).IsThreeCycle
⊢ (↑(g ^ 2)).IsThreeCycle

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).IsThreeCycle
⊢ (↑g * ↑g).IsThreeCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 3

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ ¬Fintype.card α = 6
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ 5 ≤ Nat.card α

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ 5 ≤ Fintype.card α
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hx
⊢ orderOf ?x = 4

Tactic:
exact orderOf_xa 0

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

Goal state before:
pp: case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0

Tactic:
simpa using

Goal state after:
case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬n = 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

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

Tactic:
apply (Nat.le_of_dvd
    (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left

Goal state after:
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (a 1) < 2 * n
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
  · simp_rw [mul_zero, orderOf_eq_zero_iff']
    intro n h
    rw [one_def, a_one_pow]
    apply mt a.inj
    have : CharZero (ZMod (2 * 0)) := ZMod.charZero
    simpa using h.ne'
  apply (Nat.le_of_dvd
    (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left
  intro h
  have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _
  rw [a_one_pow] at h1
  injection h1 with h2
  rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2
  exact absurd h2.symm (orderOf_pos _).ne

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : IsZGroup G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
Q : Sylow p G
hQ : P ≤ ↑Q
⊢ IsCyclic ↥P

Tactic:
exact Subgroup.isCyclic_of_le hQ

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H.toSubmonoid
⊢ n = 0 ∨ g ∈ H.toSubmonoid

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H.toSubmonoid
⊢ n = 0 ∨ g ∈ H
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H.toSubmonoid
⊢ g ^ ↑n ∈ H

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H.toSubmonoid
⊢ g ^ n ∈ H
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ ↑n ∈ H
⊢ ↑n = 0 ∨ g ∈ H

Tactic:
simpa using

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ ↑n ∈ H
⊢ n = 0 ∨ g ∈ H
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ ↑n ∈ H
⊢ g ^ n ∈ H.toSubmonoid

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ ↑n ∈ H
⊢ g ^ n ∈ H
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ (-↑n) ∈ H
⊢ -↑n = 0 ∨ g ∈ H

Tactic:
simpa using

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ (-↑n) ∈ H
⊢ n = 0 ∨ g ∈ H
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ (-↑n) ∈ H
⊢ g ^ n ∈ H.toSubmonoid

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ (-↑n) ∈ H
⊢ g ^ n ∈ H
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Nat.card α
⊢ 3 ≤ Nat.card α

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Nat.card α
⊢ 3 ≤ Fintype.card α
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)
m₁✝ m₂✝ : PushoutI φ
h : ∀ (a : NormalWord d), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
simpa using

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)
m₁✝ m₂✝ : PushoutI φ
h : ∀ (a : NormalWord d), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝
Module: Mathlib.InformationTheory.Coding.UniquelyDecodable

Goal state before:
pp: α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
⊢ ¬[] ∈ S

Tactic:
simpa using

Goal state after:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
⊢ ¬[] ∈ S
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⁆
h : Subgroup.map (commutator ↥H).subtype (commutator ↥(commutator ↥H)) ≤ Subgroup.centralizer ↑(commutator ↥H)
⊢ commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥H)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : Subgroup.map (commutator ↥H).subtype (commutator ↥(commutator ↥H)) ≤ Subgroup.centralizer ↑(commutator ↥H)
⊢ ∀ (a : G) (b : a ∈ H) (b_1 : ⟨a, b⟩ ∈ commutator ↥H),
    ⟨⟨a, b⟩, b_1⟩ ∈ commutator ↥(commutator ↥H) →
      ∀ (a_2 : G) (b : a_2 ∈ H), ⟨a_2, b⟩ ∈ commutator ↥H → a_2 * a = a * a_2
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case cons.refine_1
ι : 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 φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ (List.map Sigma.fst w'.toList).head? ≠ some i

Tactic:
hw'map,

Goal state after:
case cons.refine_1
ι : 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 φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ (List.map Sigma.fst w.toList).head? ≠ some i
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 = ∑' (b : ι × ℕ), (((κs b.1).seq b.2) a) s

Tactic:
ENNReal.summable.tsum_prod' fun _ => ENNReal.summable

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 : ι) (c : ℕ), (((κs (b, c).1).seq (b, c).2) a) s
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : ↑(hammingDist (ofHamming a✝) (ofHamming b✝)) < 1
⊢ (a✝, b✝) ∈ SetRel.id

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : ↑(hammingDist (ofHamming a✝) (ofHamming b✝)) < 1
⊢ a✝ = b✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.id ∘ₖ κ) a) s = (κ a) s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator 1 b ∂κ a = (κ a) s
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case left
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
this : ∑ x, 1 ≤ ∑ i, (↑(w i)).length
⊢ r ≤ ∑ i, (↑(w i)).length

Tactic:
simpa using

Goal state after:
case left
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
this : ∑ x, 1 ≤ ∑ i, (↑(w i)).length
⊢ r ≤ ∑ i, (↑(w i)).length