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

Goal state before:
pp: case zero
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α 0
s : Set α
hs : s.ncard = 0
⊢ (fixingSubgroup G s).index * (Nat.card α - 0)! = (Nat.card α)!

Tactic:
| zero =>

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

Goal state before:
pp: case hα
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ k + 1 ≤ Nat.card α

Tactic:
← hs,

Goal state after:
case hα
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ s.ncard ≤ Nat.card α
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ t.ncard + 1 = k + 1

Tactic:
← hs,

Goal state after:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ t.ncard + 1 = s.ncard
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
⊢ Injective ⇑(map_ofFixingSubgroupUnion M s t)

Tactic:
intro a

Goal state after:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a : ↥(ofFixingSubgroup M (s ∪ t))
⊢ ∀ ⦃a₂ : ↥(ofFixingSubgroup M (s ∪ t))⦄,
    (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) a₂ → a = a₂
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + ↑m = ↑n

Tactic:
← hs,

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + ↑m = ↑(s.ncard + m)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case zero
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hn : IsMultiplyPreprimitive M α 0
hmn : m ≤ 0
hα : ↑0 ≤ ENat.card α
⊢ IsMultiplyPreprimitive M α m

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
s : Set α
⊢ ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer (Perm α) s, g • a = b

Tactic:
intro a

Goal state after:
α : Type u_2
s : Set α
a : α
⊢ a ∈ s → ∀ b ∈ s, ∃ g ∈ stabilizer (Perm α) s, g • a = b
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
⊢ ∀ a ∈ t, ∀ b ∈ t, ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
⊢ a ∈ t → ∀ b ∈ t, ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case hs
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b

Tactic:
intro a

Goal state after:
case hs
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
⊢ a ∈ s → ∀ b ∈ s, ∃ g, g • a = b
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case zero
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = 0 + 1
hsn' : 0 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
⊢ IsMultiplyPreprimitive G α (0 + 2)

Tactic:
| zero =>

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

Goal state before:
pp: case hs'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b

Tactic:
intro a

Goal state after:
case hs'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
⊢ a ∈ sᶜ → ∀ b ∈ sᶜ, ∃ g, g • a = b
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
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
⊢ ¬B.Subsingleton → B = univ

Tactic:
intro hB'

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 : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ B = univ
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
⊢ ¬B.Subsingleton → B = univ

Tactic:
intro hB'

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ B = univ
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := ⋯
f : α →ₑ[⇑φ] α := ⋯
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
⊢ _root_.Set.univ ⊆ fixedPoints K α

Tactic:
intro a

Goal state after:
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
a : α
⊢ a ∈ _root_.Set.univ → a ∈ fixedPoints K α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
⊢ Subsingleton ↑(powersetCard α n)

Tactic:
rw [not_le] at hn'

Goal state after:
case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : Nat.card α < n
⊢ Subsingleton ↑(powersetCard α n)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ ∀ (a : ↥A),
    ⟨HNNExtension.t, t⟩ * (HNNExtension.of.codRestrict S of) ↑a =
      (HNNExtension.of.codRestrict S of) ↑(φ a) * ⟨HNNExtension.t, t⟩

Tactic:
intro a

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
a : ↥A
⊢ ⟨HNNExtension.t, t⟩ * (HNNExtension.of.codRestrict S of) ↑a =
    (HNNExtension.of.codRestrict S of) ↑(φ a) * ⟨HNNExtension.t, t⟩
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case zero
G : Type u_1
inst✝ : Group G
⊢ ∀ {H : Subgroup G},
    (∃ f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f 0 = ⊤) → H.IsSubnormal

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 ≤ mk b.1 b.2
hbc : mk b.1 b.2 ≤ mk c.1 c.2
⊢ mk a.1 a.2 ≤ mk c.1 c.2

Tactic:
by
      simp only [mk_le_mk] at hab hbc ⊢
      apply le_of_mul_le_mul_left' _
      · exact ↑b.2
      grw [mul_left_comm, hab]
      rwa [mul_left_comm, mul_left_comm (b.2 : α), mul_le_mul_iff_left]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ¬Cancels u w

Tactic:
simp only [Cancels, Option.map_eq_some_iff, Prod.exists,
    exists_and_right, exists_eq_right, not_and, not_exists]
  intro hw x hx
  rw [hx] at h2
  simpa using h2 (-u) rfl hw

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

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

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
⊢ ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a

Tactic:
intro a

Goal state after:
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
a : List ℕ
⊢ ∀ (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case mul
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hm : Irreducible (f (i * a))
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

Tactic:
rw [map_mul, irreducible_mul_iff] at hm

Goal state after:
case mul
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hm : Irreducible (f i) ∧ IsUnit (f a) ∨ Irreducible (f a) ∧ IsUnit (f i)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
x : N
hx : x ∈ Multiset.map (⇑f) (factors m) ∧ ¬IsUnit x
⊢ Prime x

Tactic:
Multiset.mem_map

Goal state after:
case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
x : N
hx : (∃ a ∈ factors m, f a = x) ∧ ¬IsUnit x
⊢ Prime x
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right.hf
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
⊢ ∀ (a a' : ℕ) (ha : a < Fintype.card α) (ha' : a' < Fintype.card α), klift a ha = klift a' ha' → a = a'

Tactic:
intro a

Goal state after:
case h.right.right.hf
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
a : ℕ
⊢ ∀ (a' : ℕ) (ha : a < Fintype.card α) (ha' : a' < Fintype.card α), klift a ha = klift a' ha' → a = a'
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ ∀ a ∈ m, 2 ≤ a

Tactic:
intro a

Goal state after:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
a : ℕ
⊢ a ∈ m → 2 ≤ a
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
⊢ ∀ (a : α), φ a = i ↔ f ((Equiv.refl α) a) = ↑i

Tactic:
intro a

Goal state after:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
a : α
⊢ φ a = i ↔ f ((Equiv.refl α) a) = ↑i
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
d : TransversalPair G A B
⊢ ∀ (a : ↥A),
    unitsSMulEquiv φ * (MulAction.toPermHom G (NormalWord d)) ↑a =
      (MulAction.toPermHom G (NormalWord d)) ↑(φ a) * unitsSMulEquiv φ

Tactic:
intro a

Goal state after:
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
d : TransversalPair G A B
a : ↥A
⊢ unitsSMulEquiv φ * (MulAction.toPermHom G (NormalWord d)) ↑a =
    (MulAction.toPermHom G (NormalWord d)) ↑(φ a) * unitsSMulEquiv φ
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
g : Perm α
⊢ ∀ (a : α), (f ∘ ⇑g) a = f a ↔ (φ ∘ ⇑g) a = φ a

Tactic:
intro a

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
g : Perm α
a : α
⊢ (f ∘ ⇑g) a = f a ↔ (φ ∘ ⇑g) a = φ a
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : 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
⊢ ∀ {a b : List α}, a ∈ p → b ∈ p → a.Disjoint b → a.formPerm.Disjoint b.formPerm

Tactic:
intro a

Goal state after:
α : 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
a : List α
⊢ ∀ {b : List α}, a ∈ p → b ∈ p → a.Disjoint b → a.formPerm.Disjoint b.formPerm
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k l : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ (k * l) • c = k • l • c

Tactic:
simp only [← Subtype.coe_inj]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k l : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ ↑((k * l) • c) = ↑(k • l • c)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ ReducedWord.prod φ w.toReducedWord • empty = w

Tactic:
induction w using consRecOn with
  | ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]
  | cons g u w h1 h2 ih =>
    rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
      of_smul_eq_smul, unitsSMul]
    rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
    -- Before https://github.com/leanprover/lean4/pull/2644, this was just
    -- simp [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
    --   -SetLike.coe_sort_coe]
    -- ext <;> simp [-SetLike.coe_sort_coe]
    simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
      (d.compl _).equiv_snd_eq_inv_mul, inv_one, one_mul, mul_inv_cancel, one_smul, smul_cons]
    ext <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ x ∈ Function.fixedPoints ⇑g ∨ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
rw [Classical.or_iff_not_imp_left]
  intro hx
  rw [Function.mem_fixedPoints_iff, ← ne_eq, ← mem_support,
    ← cycleOf_mem_cycleFactorsFinset_iff] at hx
  refine ⟨⟨g.cycleOf x, hx⟩, ?_, (a.sameCycle hx)⟩
  rw [mem_support_cycleOf_iff, ← cycleOf_mem_cycleFactorsFinset_iff]
  simp [SameCycle.rfl, hx, and_self]

Goal state after:
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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then (g ^ Nat.find ⋯) (a (↑τ ⟨g.cycleOf x, hx⟩)) else x) = x

Tactic:
dif_neg

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x = x

case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ g.cycleOf x ∉ g.cycleFactorsFinset