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

Goal state before:
pp: case inr.hsn'
α : 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
⊢ n + 2 < Nat.card α

Tactic:
grind

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

Goal state before:
pp: case inr.inr.hmn
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ n ≤ Nat.card α - 2

Tactic:
grind

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

Goal state before:
pp: case inr.inr.hα
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ Nat.card α - 2 ≤ Nat.card α

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
by
  wlog! hn : 2 * n ≤ Nat.card α
  · have : IsPretransitive (alternatingGroup α) (powersetCard α (Nat.card α - n)) := by
      apply this hα
      grind
    by_cases hn' : n ≤ Nat.card α
    · apply IsPretransitive.of_surjective_map
        (mulActionHom_compl_bijective (alternatingGroup α) α _).surjective this
      aesop
    · suffices Subsingleton (powersetCard α n) by infer_instance
      rw [not_le] at hn'
      rw [← Finite.card_le_one_iff_subsingleton, powersetCard.card,
        Nat.choose_eq_zero_iff.mpr hn']
      simp
  apply isPretransitive_of_isMultiplyPretransitive
  rcases eq_or_ne n 0 with rfl | hn0
  · infer_instance
  rcases eq_or_ne n 1 with rfl | hn1
  · rw [is_one_pretransitive_iff]
    exact alternatingGroup.isPretransitive_of_three_le_card α hα
  have := alternatingGroup.isMultiplyPretransitive α
  apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) <;> grind

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

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

Tactic:
by
  match n with
  | 0 => simp
  | n + 1 =>
    rw [derivedSeries_succ, derivedSeries_eq_top, commutator_eq_self]

Goal state after:
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
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
by
  have : IsPretransitive (alternatingGroup α) (powersetCard α n) :=
    isPretransitive_alternatingGroup (le_trans h_three_le hn.le)
  have : Nontrivial (powersetCard α n) := nontrivial (by positivity) (by simpa using hn)
  obtain ⟨s⟩ := this.to_nonempty
  rw [← isCoatom_stabilizer_iff_preprimitive _ s, stabilizer_coe]
  apply alternatingGroup.isCoatom_stabilizer
  · rw [powersetCard.coe_nonempty_iff]
    exact le_trans (by norm_num) h_three_le
  · simpa [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq] using ne_of_lt hn
  · simpa only [ncard_eq]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊥
hSubn : ⊥.IsSubnormal
hN : (H.subgroupOf ⊥).Normal
Knorm : ⊥.Normal
⊢ H.Normal

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsSimpleGroup G
hN : H.IsSubnormal
⊢ H.Normal

Tactic:
by
  induction hN with
  | top => simp
  | step H K h_le hSubn hN Knorm =>
    obtain rfl | rfl := Knorm.eq_bot_or_eq_top
    · grind
    · grind [!normal_subgroupOf_iff_le_normalizer_inf, inf_of_le_left, normalizer_eq_top_iff]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K ≠ ⊤ → ∃ K_1, K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
K_ne : K ≠ ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: 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) =
      ⊤

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: 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

Tactic:
grind

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
d : TransversalPair G A B
g : G
⊢ (unitsSMulGroup φ d 1 g).2 = (⋯.equiv g).2

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

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

Tactic:
rfl

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

Goal state before:
pp: case f.H
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a✝¹ : α
b✝¹ : ↥s
a✝ c✝ : α
b✝ d✝ : ↥s
h✝ : (r s) (a✝, b✝) (c✝, d✝)
⊢ ⋯ = ⋯

Tactic:
rfl

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a b : Localization s
a✝ c✝ : α
b✝ d✝ : ↥s
h✝ : (r s) (a✝, b✝) (c✝, d✝)
⊢ ⋯ = ⋯

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
m : M
hm : Irreducible (f m)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ m = u * m'

Tactic:
by
  induction m using WfDvdMonoid.induction_on_irreducible with
  | zero => exact (hm.ne_zero f.map_zero).elim
  | unit u hu => exact (hm.not_isUnit (hu.map f)).elim
  | mul a i ha0 hi ha =>
    rw [map_mul, irreducible_mul_iff] at hm
    obtain hia | hai := hm
    · exact ⟨a, i, hia.2, hi, mul_comm ..⟩
    · obtain ⟨u, m', hu, hm', rfl⟩ := ha hai.1
      exact ⟨u * i, m', by simpa using hu.mul hai.2, hm', by ac_rfl⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g • f = f ↔ f ∘ ⇑(mk.symm g) = f

Tactic:
rfl

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 : α
⊢ stabilizerEquiv_invFun g a = ↑((g (f a)) ⟨a, ⋯⟩)

Tactic:
rfl

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 ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ mk x✝ ∈ stabilizer (Perm α)ᵈᵐᵃ f

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
g✝ : G
u✝ : ℤˣ
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set u✝
h2✝ : ∀ u' ∈ Option.map Prod.fst w✝.toList.head?, w✝.head ∈ toSubgroup A B u✝ → u✝ = u'
this : Cancels 1 (↑g • cons g✝ u✝ w✝ h1✝ h2✝) ↔ Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
hcan : Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g_1 a ↦ ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
      ↑(φ g) •
        consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝)
          (fun g a ↦ cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan
⊢ ↑(φ ⟨↑g * g✝, ⋯⟩) • w✝ = ↑(φ (g * ⟨g✝, ⋯⟩)) • w✝

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.e_w
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (↑(g * (⋯.equiv w.head).1, (⋯.equiv w.head).2).2 * w.head⁻¹) • w = (↑(⋯.equiv w.head).2 * w.head⁻¹) • w

Tactic:
rfl

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

Goal state before:
pp: case h
α : 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.map (fun l ↦ l.formPerm) p).prod.cycleType = m

Tactic:
Equiv.Perm.cycleType_eq _ rfl

Goal state after:
case h
α : 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.map (Finset.card ∘ support) (List.map (fun l ↦ l.formPerm) p)) = m

case h.h1
α : 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.map (fun l ↦ l.formPerm) p, σ.IsCycle

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)
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : 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
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]

Tactic:
grind

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

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
⊢ y ∈ {x | Equiv.swap x y ∈ closure S}

Tactic:
mem_ofPred,

Goal state after:
case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
⊢ Equiv.swap y y ∈ closure S
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)

Tactic:
simp only [ofPermHomFun_apply_of_mem_fixedPoints a _ hx]

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 : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑(σ * τ) c)) = (g ^ m) (a (↑σ (↑τ c)))

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ (Finset.univ.noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
← Finset.noncommProd_erase_mul _ (Finset.mem_univ ⟨g.cycleOf x, hx⟩),

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯ * ↑((u, v).2 ⟨g.cycleOf x, hx⟩)) x =
    ↑(v ⟨g.cycleOf x, hx⟩) x
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : ¬Even (m.sum + m.card)
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∏ i, Fintype.card ↥(zpowers ↑i) = g.cycleType.prod

Tactic:
rw [Finset.univ_eq_attach, g.cycleFactorsFinset.prod_attach (fun i ↦ Fintype.card (zpowers i)),
    cycleType, Finset.prod_map_val]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∏ x ∈ g.cycleFactorsFinset, Fintype.card ↥(zpowers x) = ∏ a ∈ g.cycleFactorsFinset, (Finset.card ∘ support) a
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x✝¹ : Group G'
x✝ : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ Nat.card G' = Nat.card G'

Tactic:
rfl

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

Goal state before:
pp: case «2»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 2 ∈ g.cycleType
hk4 : 2 ≤ 4
hk1 : 1 < 2
⊢ 2 = 2

Tactic:
rfl

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

Goal state before:
pp: case h_one_le
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

Tactic:
grind

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

Goal state before:
pp: case hn
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 2 < Nat.card α

Tactic:
grind

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

Goal state before:
pp: case hα
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 2

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
this : IsPreprimitive (Perm α) ↑(Set.powersetCard α 2)
⊢ 2 < Nat.card α

Tactic:
grind

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

Goal state before:
pp: case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
this : 2 * ↑n = 0
⊢ xa (k - ↑n - j + i) = xa (k + ↑n - j + i)

Tactic:
grind

Goal state after:
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)
⊢ 3 < Nat.card α

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ a 0 = 1

Tactic:
rfl

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

Goal state before:
pp: case inl
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i ↦
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inl x)) =
    Sum.inl x

Tactic:
rfl

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

Goal state before:
pp: case inr
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i ↦
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inr x)) =
    Sum.inr x

Tactic:
rfl

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

Goal state before:
pp: case a
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i ↦
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (a x)) =
    a x

Tactic:
rfl

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

Goal state before:
pp: case xa
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i ↦
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (xa x)) =
    xa x

Tactic:
rfl

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

Goal state before:
pp: case a
n : ℕ
k : ZMod (2 * 0)
⊢ (fun x ↦
        match x with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun x ↦
          match x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (a k)) =
    a k

Tactic:
rfl

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

Goal state before:
pp: case xa
n : ℕ
k : ZMod (2 * 0)
⊢ (fun x ↦
        match x with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun x ↦
          match x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (xa k)) =
    xa k

Tactic:
rfl

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

Goal state before:
pp: case r
n : ℕ
k : ZMod 0
⊢ (fun x ↦
        match x with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun x ↦
          match x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.r k)) =
    DihedralGroup.r k

Tactic:
rfl

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

Goal state before:
pp: case sr
n : ℕ
k : ZMod 0
⊢ (fun x ↦
        match x with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun x ↦
          match x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.sr k)) =
    DihedralGroup.sr k

Tactic:
rfl

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

Goal state before:
pp: case zero
n : ℕ
⊢ a 1 ^ 0 = a 0

Tactic:
rfl

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

Goal state before:
pp: case hn
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ 4 < Nat.card α

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hα' : Nat.card α = 6
⊢ Nat.card α ≠ 8

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
x : PushoutI φ
g₁ : G i
hg₁ : (of i) g₁ = x
g₂ : G j
hg₂ : (of j) g₂ = x
hx : ¬x ∈ (base φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := { toList := [⟨i, g₁⟩, ⟨j, g₂⁻¹⟩], ne_one := ⋯, chain_ne := ⋯ }
hw : Reduced φ w
this : w = Word.empty
⊢ False

Tactic:
simp [w, Word.empty] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → β
hf : Measurable f
h : f = g
⊢ deterministic f hf = deterministic g ⋯

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : i = 0
⊢ (κ a) s = (κ a) s

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : ¬i = 0
⊢ (0 a) s = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
⊢ Function.Injective concatFn

Tactic:
by
  intro w₁ w₂ hflat
  funext i
  have := List.ofFn_injective (h _ _ (by simp) (by simp) hflat)
  exact Subtype.ext (congrArg (fun f => f i) this)

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
h✝ : a ∈ s
⊢ (κ a) t = (κ a) t

Tactic:
rfl

Goal state after: