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

Goal state before:
pp: case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ s
k : M
hk : k ∈ fixingSubgroup M s
hkax : ⟨k, hk⟩ • ⟨a, ⋯⟩ = ⟨x, hx⟩
⊢ ⟨k, ⋯⟩ • ⟨a, ha'⟩ = ⟨x, hx✝⟩

Tactic:
Subtype.ext_iff

Goal state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ s
k : M
hk : k ∈ fixingSubgroup M s
hkax : ↑(⟨k, hk⟩ • ⟨a, ⋯⟩) = ↑⟨x, hx⟩
⊢ ↑(⟨k, ⋯⟩ • ⟨a, ha'⟩) = ↑⟨x, hx✝⟩
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
⊢ ∃ g, g • x = y

Tactic:
· have : (Finset.univ.image x)ᶜ.card = 2 := by
      rw [Finset.card_compl, Finset.univ.card_image_of_injective (by exact x.2), Finset.card_univ,
        ← Nat.card_eq_fintype_card, Fintype.card_fin, tsub_tsub_cancel_of_le h2]
    obtain ⟨a, b, hab, hs⟩ := Finset.card_eq_two.mp this
    refine ⟨⟨g * Equiv.swap a b, by simp [h, hab]⟩, ?_⟩
    ext i
    have h : x i ∈ Finset.univ.image x := Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩
    rw [← Finset.notMem_compl, hs, Finset.mem_insert, Finset.mem_singleton, not_or] at h
    simp [Equiv.swap_apply_of_ne_of_ne h.1 h.2, ← hg]

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 α
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
x : α
hx : x ∈ s
hy : f x ∈ t
⊢ φ g • f x = f x

Tactic:
rwa [← map_smulₛₗ, hg]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : 2 < s.ncard
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle

Tactic:
two_lt_ncard_iff

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : univ.encard = 2
⊢ univ.Finite

Tactic:
exact finite_of_encard_eq_coe hα

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

Goal state before:
pp: case inr.inr.inl
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝ : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card (Perm α)))
h : G = ⊥
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
exfalso

Goal state after:
case inr.inr.inl
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝ : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card (Perm α)))
h : G = ⊥
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : sᶜ.Nontrivial
a : α
ha : a ∈ s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

Tactic:
obtain ⟨b, hb, c, hc, hbc⟩ := hsc

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ G = ⊤

Tactic:
have hG' : stabilizer (Perm α) sᶜ < G := by rwa [stabilizer_compl]

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
⊢ G = ⊤
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case refine_1
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ t.ncard = n + 1

Tactic:
← Set.ncard_image_of_injective t Subtype.val_injective

Goal state after:
case refine_1
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ (Subtype.val '' t).ncard = n + 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

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

Tactic:
by_cases h0' : s.Nontrivial
    · apply isCoatom_stabilizer_of_ncard_lt_ncard_compl h0' hs'
    · simp only [not_nontrivial_iff] at h0'
      apply isCoatom_stabilizer_singleton _ h0 h0'
      rw [← ncard_add_ncard_compl s]
      rw [← ncard_pos] at h0 h1
      grind

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
stabilizer_coe

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer (Perm α) ↑s)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G →* G'
inst✝ : IsPerfect ↥H
⊢ map f ⁅H, H⁆ = map f H

Tactic:
commutator_eq_self

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G →* G'
inst✝ : IsPerfect ↥H
⊢ map f H = map f H
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ ⁅⊤, ⊤⁆ = ⊤

Tactic:
commutator_eq_self

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ ⊤ = ⊤
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
stabilizer_coe

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer ↥(alternatingGroup α) ↑s)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n✝ n : ℕ
⊢ ⁅H, H⁆ = H

Tactic:
commutator_eq_self

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n✝ n : ℕ
⊢ H = H
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 n = center G

Tactic:
rw [← Subgroup.upperCentralSeries_one, eq_comm]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ Subgroup.upperCentralSeries G 1 = Subgroup.upperCentralSeries G n
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst✝¹ : (i : ι) → CommMonoid (M i)
inst✝ : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
x y : (i : ι) → M i
eq : Pi.map f x = Pi.map f y
c : (i : ι) → ↥(S i)
hc : ∀ (i : ι), ↑(c i) * x i = ↑(c i) * y i
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
exact ⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∏ a, Nat.card (Perm { a_1 // f a_1 = a }) = ∏ i, (Fintype.card { a // f a = i })!

pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ mk x✝ ∈ stabilizer (Perm α)ᵈᵐᵃ f

Tactic:
· exact Finset.prod_congr rfl fun i _ ↦ by rw [Nat.card_eq_fintype_card, Fintype.card_perm]

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ mk x✝ ∈ stabilizer (Perm α)ᵈᵐᵃ f
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑((toSubgroupEquiv φ 1) (⋯.equiv w.head).1) *
      (t ^ ↑1 * (of ↑(⋯.equiv w.head).2 * (of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    t ^ ↑1 * ReducedWord.prod φ w.toReducedWord

Tactic:
simp only [toSubgroup_neg_one, toSubgroup_one, toSubgroupEquiv_one, equiv_eq_conj, mul_assoc,
        Units.val_one, zpow_one, inv_mul_cancel_left, mul_right_inj]

Goal state after:
case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑(⋯.equiv w.head).1 * (of ↑(⋯.equiv w.head).2 * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S

Tactic:
revert f

Goal state after:
case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
⊢ ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S
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 : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ (j + m)) (a c) = (g ^ j) x

Tactic:
zpow_add,

Goal state after:
α : 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
⊢ (g ^ j * g ^ m) (a c) = (g ^ j) x
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, (toPermHom G α) σ = 1 ∨ ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h✝ : IsPretransitive G α
h : closure (⇑(toPermHom G α) '' S \ {1}) = (toPermHom G α).range
this : IsPretransitive (↥(toPermHom G α).range) α
⊢ Function.Surjective ⇑(toPermHom G α)

Tactic:
rw [← h] at this

Goal state after:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, (toPermHom G α) σ = 1 ∨ ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h✝ : IsPretransitive G α
h : closure (⇑(toPermHom G α) '' S \ {1}) = (toPermHom G α).range
this : IsPretransitive (↥(closure (⇑(toPermHom G α) '' S \ {1}))) α
⊢ Function.Surjective ⇑(toPermHom G α)
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 = {1} ∪ {g | (↑g).cycleType = {2, 2}}

Tactic:
classical
  refine Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_
  · -- inclusion S ⊆ {1} ∪ {g |  cycleType g = { 2, 2 }}
    obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩
    replace hn : (orderOf (k : Perm α)) = 2 ^ n := by simpa using hn
    convert! mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd
    simp
  · -- card (kleinFour α) ≤ card S
    simp_rw [← Nat.card_eq_fintype_card]
    refine (card_two_sylow_of_card_eq_four hα4 S).trans_ge ?_
    rw [Nat.card_eq_card_toFinset, Set.toFinset_union, Set.toFinset_singleton, Set.toFinset_ofPred]
    apply (Finset.card_union_le _ _).trans
    rw [Finset.card_singleton, AlternatingGroup.card_of_cycleType, ← Nat.card_eq_fintype_card, hα4]
    decide

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : IsZGroup G
hf : Function.Surjective ⇑f
⊢ IsZGroup G'

Tactic:
by
  rw [isZGroup_iff] at hG ⊢
  intro p hp P
  have := Fact.mk hp
  obtain ⟨Q, rfl⟩ := Sylow.mapSurjective_surjective hf p P
  specialize hG p hp Q
  exact isCyclic_of_surjective _ (f.subgroupMap_surjective Q)

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
⊢ (Nat.card ↥(commutator G)).Coprime (commutator G).index

Tactic:
suffices h : ∀ p, p.Prime → (¬ p ∣ Nat.card (commutator G) ∨ ¬ p ∣ (commutator G).index) by
    contrapose! h
    exact Nat.Prime.not_coprime_iff_dvd.mp h
  intro p hp
  have := Fact.mk hp
  exact Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator default

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s

Tactic:
Kernel.ext_iff,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ (∀ (a : α), κ a = η a) ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ (∀ ⦃x_1 : ι⦄, x_1 ∈ univ → x x_1 = y x_1) → x = y

Tactic:
funext_iff,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ (∀ ⦃x_1 : ι⦄, x_1 ∈ univ → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ NullMeasurableSet (Prod.mk a ⁻¹' t) (κ a)

pp: case h_fin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (κ a) (Prod.mk a ⁻¹' t) ≠ ∞

Tactic:
· exact (measurable_prodMk_left htm).nullMeasurableSet

Goal state after:
case h_fin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (κ a) (Prod.mk a ⁻¹' t) ≠ ∞
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (Kernel.piecewise hs κ η)

Tactic:
by
  refine ⟨⟨max κ.bound η.bound, max_lt κ.bound_lt_top η.bound_lt_top, fun a => ?_⟩⟩
  rw [piecewise_apply']
  exact (ite_le_sup _ _ _).trans (sup_le_sup (measure_le_bound _ _ _) (measure_le_bound _ _ _))

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 α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ IsSFiniteKernel (piecewise hs κ η)

Tactic:
refine ⟨⟨fun n => piecewise hs (seq κ n) (seq η n), inferInstance, ?_⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ Measurable fun a ↦ ∫⁻ (b : β), (F n) (a, b) ∂κ a

Tactic:
refine SimpleFunc.induction
    (motive := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ ∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s),
    Measurable fun a ↦
      ∫⁻ (b : β), (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0)) (a, b) ∂κ a

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ ∀ ⦃f g : SimpleFunc (α × β) ℝ≥0∞⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (Measurable fun a ↦ ∫⁻ (b : β), f (a, b) ∂κ a) →
        (Measurable fun a ↦ ∫⁻ (b : β), g (a, b) ∂κ a) → Measurable fun a ↦ ∫⁻ (b : β), (f + g) (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.MapComap

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

Tactic:
simp [map_apply, measurable_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ κ.map ⇑f = η ↔ κ = η.map ⇑f.symm

Tactic:
Kernel.ext_iff,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ (∀ (a : α), (κ.map ⇑f) a = η a) ↔ ∀ (a : α), κ a = (η.map ⇑f.symm) a
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
by
  by_cases hμ : SFinite μ
  · simp_rw [Measure.compProd, Kernel.prodMkLeft_add, Kernel.compProd_add_right, _root_.add_apply]
  · simp [hμ]

Goal state after:
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : β), IsMarkovKernel (κ.sectL b)
⊢ IsMarkovKernel κ

Tactic:
by
  refine ⟨fun _ ↦ ⟨?_⟩⟩
  rw [← sectL_apply, measure_univ]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
inst✝ : IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ κ

Tactic:
rw [parallelComp_id_left_comp_parallelComp]
  congr
  exact comp_id κ

Goal state after: