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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
t : Set ↥(ofStabilizer G a)
⊢ a ∉ Subtype.val '' t

Tactic:
by
  rintro ⟨b, hb⟩
  exact b.prop (by simp [hb])

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
g : H
this : (Set.range ⇑f ∩ g • B).Subsingleton
⊢ (Set.range ⇑f ∩ ↑⟨(fun g ↦ g • B) g, ⋯⟩).ncard ≤ 1

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ IsMultiplyPretransitive (Perm α) α n

Tactic:
by
  rw [isMultiplyPretransitive_iff]
  exact exists_smul_eq_embedding

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)

Tactic:
by
  rcases lt_or_ge (Nat.card α) 2 with h2 | h2
  · rw [Nat.sub_eq_zero_of_le (le_of_lt h2)]
    apply is_zero_pretransitive
  have h2le : Nat.card α - 2 ≤ Nat.card α := sub_le (Nat.card α) 2
  have := Equiv.Perm.isMultiplyPretransitive α (Nat.card α)
  have : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2) :=
    MulAction.isMultiplyPretransitive_of_le h2le le_rfl
  refine ⟨fun x y ↦ ?_⟩
  obtain ⟨g, hg⟩ := exists_smul_eq (Equiv.Perm α) x y
  rcases Int.units_eq_one_or (Equiv.Perm.sign g) with h | h
  · exact ⟨⟨g, h⟩, hg⟩
  · 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.Period

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
fixed : m • a = a
⊢ m ^ 1 • a = a

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
k : Perm α
hk : k ∈ stabilizer (Perm α) s
h : ↥G := ⟨k, ⋯⟩
this : h ∈ stabilizer (↥G) s
⊢ ∃ a, toPerm a = toPerm ⟨k, hk⟩

Tactic:
exact ⟨⟨h, this⟩, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
hH : H ≠ ⊤
⊢ H < ⊤ ∧ ⊤.IsSubnormal ∧ (H.subgroupOf ⊤).Normal

Tactic:
by simp [hH.lt_top , *]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
⊢ (let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

Tactic:
· have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 hcan)
    unfold unitsSMul at hcan ⊢
    simp only [dif_pos hcan2] at hcan ⊢
    cases w using consRecOn with
    | ofGroup => simp [Cancels] at hcan2
    | cons g u' w h1 h2 ih =>
      clear ih
      simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, consRecOn_cons,
        group_smul_head,
        mul_inv_rev]
      cases hcan2.2
      have : ((d.compl (-u)).equiv w.head).1 = 1 :=
        (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1
      simpa [NormalWord.ext_iff, (d.compl (-u)).equiv_mul_left, Units.ext_iff,
        (d.compl (-u)).equiv_snd_eq_inv_mul]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels u w
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord = t ^ ↑u * ReducedWord.prod φ w.toReducedWord

pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels u w
⊢ ReducedWord.prod φ
      (let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord

Tactic:
· cases w using consRecOn
    · simp [Cancels] at hcan
    · cases hcan.2
      simp only [unitsSMulWithCancel, id_eq, consRecOn_cons, prod_group_smul, prod_cons, zpow_neg]
      rcases Int.units_eq_one_or u with (rfl | rfl)
      · simp [equiv_eq_conj, mul_assoc]
      · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
        -- simp [equiv_symm_eq_conj, mul_assoc].
        simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
          Int.reduceNeg, zpow_neg, zpow_one, inv_inv]
        erw [equiv_symm_eq_conj, mul_assoc, mul_assoc]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels u w
⊢ ReducedWord.prod φ
      (let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
x✝¹ : Perm α
x✝ : x✝¹ ∈ g.cycleFactorsFinset
⊢ ((MulAction.toPermHom ↥(centralizer {g}) ↥g.cycleFactorsFinset) k) ⟨x✝¹, x✝⟩ = 1 ⟨x✝¹, x✝⟩ ↔ Commute (↑k) x✝¹

Tactic:
simp [← Subtype.coe_inj, commute_iff_eq, mul_inv_eq_iff_eq_mul]

Goal state after:
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 α
⊢ Function.Surjective ⇑(toPermHom G α)

Tactic:
by
  have h : closure ((toPermHom G α '' S) \ {1}) = (toPermHom G α).range := by
    rw [closure_sdiff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
  have := IsPretransitive.of_compHom (α := α) (toPermHom G α).rangeRestrict
  rw [← h] at this
  rw [← MonoidHom.range_eq_top, ← h, closure_of_isSwap_of_isPretransitive]
  rintro - ⟨⟨σ, hσ, rfl⟩, hσ1⟩
  exact (hS1 σ hσ).resolve_left hσ1

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ 1 * a = a

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ a * 1 = a

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ a⁻¹ * a = 1

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝¹ x✝ : Q
⊢ { left := 1, right := x✝¹ * x✝ } = { left := 1, right := x✝¹ } * { left := 1, right := x✝ }

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ (fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
      ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x) =
    x

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ (fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
      ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x) =
    x

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right } =
    { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } * { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }

Tactic:
by ext <;> simp

Goal state after:
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
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : ResiduallyFinite G
H : Subgroup G
g : ↥H
hg : ∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1
⊢ ↑g = ↑1

Tactic:
exact eq_one_iff_forall_finiteIndexNormalSubroup g.1 fun K ↦ hg (K.comap H.subtype)

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
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
kerParam,

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
⊢ ((ofSubtype.noncommCoprod (noncommPiCoprod ⋯) ⋯) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((kerParam g) (u, v)) x = (ofSubtype u) x

Tactic:
kerParam,

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((ofSubtype.noncommCoprod (noncommPiCoprod ⋯) ⋯) (u, v)) x = (ofSubtype u) x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(kerParam g)

Tactic:
kerParam,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(ofSubtype.noncommCoprod (noncommPiCoprod ⋯) ⋯)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range ≤ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
kerParam,

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (ofSubtype.noncommCoprod (noncommPiCoprod ⋯) ⋯).range ≤ map (centralizer {g}).subtype (toPermHom g).ker
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign ((kerParam g) (k, v)) = sign k * ∏ c, sign ↑(v c)

Tactic:
kerParam,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign ((ofSubtype.noncommCoprod (noncommPiCoprod ⋯) ⋯) (k, v)) = sign k * ∏ c, sign ↑(v c)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c, (↑(v c)).cycleType

Tactic:
let U := SetLike.coe (Finset.univ : Finset { x // x ∈ g.cycleFactorsFinset })

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c, (↑(v c)).cycleType
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
hU : U.Pairwise fun i j ↦ (↑(v i)).Disjoint ↑(v j)
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c, (↑(v c)).cycleType

Tactic:
kerParam,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
hU : U.Pairwise fun i j ↦ (↑(v i)).Disjoint ↑(v j)
⊢ ((ofSubtype.noncommCoprod (noncommPiCoprod ⋯) ⋯) (k, v)).cycleType = k.cycleType + ∑ c, (↑(v c)).cycleType
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
← nat_card_centralizer g

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↑{h | IsConj g h} * Nat.card ↥(centralizer {g}) = (Fintype.card α)!
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 0 <
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
← nat_card_centralizer g

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 0 < Nat.card ↥(centralizer {g})
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case neg
ι : 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
hep : ¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = i
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
· push Not at hep
        by_cases hw : w.toList = []
        · simp [hw, Word.fstIdx]
        · simp [head?_eq_some_head hw, Word.fstIdx, hep hw]

Goal state after:
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
⊢ n ! = (n - 1)! * n

Tactic:
rw [mul_comm, mul_factorial_pred hn₀]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ (g • s).card = 4

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2

Tactic:
by
  rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]
  simp only [Nat.reduceMul]
  rcases eq_zero_or_neZero n with rfl | hn
  · simp only [lcm_zero_left, mul_zero]
    exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one
  apply Nat.dvd_antisymm
  · apply Monoid.exponent_dvd_of_forall_pow_eq_one
    rintro (m | m)
    · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]
      refine Nat.dvd_trans ⟨gcd (2 * n) m.val, ?_⟩ (dvd_lcm_left (2 * n) 4)
      exact (Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm
    · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]
      exact dvd_lcm_right (2 * n) 4
  · apply lcm_dvd
    · convert! Monoid.order_dvd_exponent (a 1)
      exact orderOf_a_one.symm
    · convert! Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))
      exact (orderOf_xa 0).symm

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
g : G
hg : g ∈ P
⊢ g ∈ ⁅K, P⁆

Tactic:
obtain ⟨k, q, hkq⟩ := h ⟨g, hg⟩

Goal state after:
case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
g : G
hg : g ∈ P
k : ↥K
q : ↥P
hkq : k • q * q⁻¹ = ⟨g, hg⟩
⊢ g ∈ ⁅K, P⁆
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
⊢ (hammingDist (fun i ↦ f i (x i)) fun i ↦ f i (y i)) ≤ hammingDist x y

Tactic:
dsimp [hammingDist]

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
⊢ #{i | ¬f i (x i) = f i (y i)} ≤ #{i | ¬x i = y i}
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ hammingDist x y ≤ hammingDist (fun i ↦ f i (x i)) fun i ↦ f i (y i)

Tactic:
dsimp [hammingDist]

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ #{i | ¬x i = y i} ≤ #{i | ¬f i (x i) = f i (y i)}
Module: Mathlib.Probability.Kernel.Basic

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

Tactic:
comapRight_apply _ hf

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ Measure.comap f (κ a) = Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ()) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

Tactic:
Kernel.compProd_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (b : α), ((Kernel.prodMkLeft Unit κ) ((), b)) (Prod.mk b ⁻¹' s) ∂(Kernel.const Unit μ) () =
    ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = (κ a ⊗ₘ η.sectR a) s

Tactic:
Kernel.compProd_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = (κ a ⊗ₘ η.sectR a) s
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 (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero ((κ.sectR a) b)

Tactic:
sectR_apply

Goal state after:
α : 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 (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero (κ (a, b))
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = 0 ↔ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0

Tactic:
Kernel.compProd_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = 0 ↔ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0