mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : CompactSpace M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)

Tactic:
rcases SmoothBumpCovering.exists_isSubordinate I isClosed_univ fun (x : M) _ => univ_mem with
    ⟨ι, f, -⟩

Goal state after:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
x : M
hU : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) x
hV : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) x
hW : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) x
⊢ mlieBracket I U (mlieBracket I V W) x = mlieBracket I (mlieBracket I U V) W x + mlieBracket I V (mlieBracket I U W) x

Tactic:
simp only [← mlieBracketWithin_univ, ← contMDiffWithinAt_univ] at hU hV hW ⊢
  exact leibniz_identity_mlieBracketWithin_apply uniqueMDiffOn_univ (by simp) (mem_univ _) hU hV hW

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

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
exact ⟨mulEquiv ((Fintype.equivOfCardEq <| by simp).setValue 1 1) <| by simp⟩

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

Goal state before:
pp: case sr
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
this : Fact (1 < n)
⊢ sr i = 1

Tactic:
simp [sub_eq_iff_eq_add, add_assoc, ZMod.add_self_eq_zero_iff_eq_zero hodd] at heq

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
⊢ (equivPair i)
      (rcons
        (have __src := (equivPair i) w;
        { head := m * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })) =
    { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }

Tactic:
← equivPair_symm

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
⊢ (equivPair i)
      ((equivPair i).symm
        (have __src := (equivPair i) w;
        { head := m * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })) =
    { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 = of m • ls

Tactic:
rw [of_smul_def, equivPair_eq_of_fstIdx_ne _]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 =
    rcons
      (have __src := { head := 1, tail := ls, fstIdx_ne := ?m.39 };
      { head := m * { head := 1, tail := ls, fstIdx_ne := ?m.39 }.head, tail := __src.tail, fstIdx_ne := ⋯ })

ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ ls.fstIdx ≠ some i
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ cs.leftInvSeq (take j ω) = take j (cs.leftInvSeq ω)

Tactic:
by
  simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse]
  rw [List.take_reverse]
  nth_rw 1 [← List.reverse_reverse ω]
  rw [List.take_reverse]
  simp [rightInvSeq_drop]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.tail
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t

Tactic:
· exact ih mem

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
⊢ Group.FG G

Tactic:
let s : Set G := Set.range qi

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
⊢ Group.FG G
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsLeftInversion (cs.wordProd ω) t

Tactic:
by
  constructor
  · exact cs.isReflection_of_mem_leftInvSeq ω ht
  · obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht
    rw [← List.getD_eq_getElem _ 1 hj, getD_leftInvSeq_mul_wordProd]
    rw [cs.length_leftInvSeq] at hj
    calc
      ℓ (π (ω.eraseIdx j))
      _ ≤ (ω.eraseIdx j).length := cs.length_wordProd_le _
      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
      _ = ℓ (π ω) := hω.symm

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hXdisj.hs.hu
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) (Y j)

pp: case hXdisj.ht.ht
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (X j)

pp: case hXdisj.ht.hu
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)

Tactic:
· exact hXYdisj i j

Goal state after:
case hXdisj.ht.ht
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (X j)

case hXdisj.ht.hu
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hpp
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
hnne0 : n ≠ 0
⊢ a i ^ n • X' j ⊆ X' i

Tactic:
clear hne1

Goal state after:
case hpp
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
⊢ a i ^ n • X' j ⊆ X' i
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroup ≤ H

Tactic:
rw [focalSubgroup_def, closure_le]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ⊆ ↑H
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroup ≤ _root_.commutator G

Tactic:
rw [focalSubgroup_def, closure_le]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ⊆ ↑(_root_.commutator G)
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, H⁆ ≤ H.focalSubgroup

Tactic:
← map_subtype_commutator,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype (_root_.commutator ↥H) ≤ H.focalSubgroup
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ → nilpotencyClass G ≤ n

pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → upperCentralSeries G n = ⊤

Tactic:
· intro h
    rw [nilpotencyClass_def]
    exact Nat.find_le h

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → upperCentralSeries G n = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
rintro n ⟨H, ⟨hH, hn⟩⟩
    refine ⟨fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
    dsimp only
    rw [tsub_self]
    exact hH.1

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
⊢ ∀ {H : Type u} [inst : Group H] (f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → H),
    ∃! F, ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a

Tactic:
by
      intro X _ f
      let f' : Labelling (Generators G) X := fun a b e =>
        if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨⟨a, b, e⟩, h⟩
      rcases unique_lift f' with ⟨F', hF', uF'⟩
      refine ⟨F'.mapEnd _, ?_, ?_⟩
      · suffices ∀ {x y} (q : x ⟶ y), F'.map (loopOfHom T q) = (F'.map q : X) by
          rintro ⟨⟨a, b, e⟩, h⟩
          simp only [Functor.mapEnd, DFunLike.coe, this, hF']
          exact dif_neg h
        intro x y q
        suffices ∀ {a} (p : Path (root T) a), F'.map (homOfPath T p) = 1 by
          simp only [this, treeHom, comp_as_mul, inv_as_inv, loopOfHom, inv_one, mul_one,
            one_mul, Functor.map_inv, Functor.map_comp]
        intro a p
        induction p with
        | nil => rw [homOfPath, F'.map_id, id_as_one]
        | cons p e ih =>
          rw [homOfPath, F'.map_comp, comp_as_mul, ih, mul_one]
          rcases e with ⟨e | e, eT⟩
          · rw [hF']
            exact dif_pos (Or.inl eT)
          · rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']
            exact dif_pos (Or.inr eT)
      · intro E hE
        ext x
        suffices (functorOfMonoidHom T E).map x = F'.map x by
          simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root,
            Category.id_comp, Category.comp_id] using! this
        congr
        apply uF'
        intro a b e
        change E (loopOfHom T _) = dite _ _ _
        split_ifs with h
        · rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
        · exact hE ⟨⟨a, b, e⟩, h⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ (upperCentralSeries G '' Set.Iic a).ncard = a + 1

Tactic:
refine Set.ncard_eq_of_bijective (fun _ => upperCentralSeries G ·) ?_ ?_ ?_

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ a_1 ∈ upperCentralSeries G '' Set.Iic a, ∃ i, ∃ (_ : i < a + 1), upperCentralSeries G i = a_1

case refine_2
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ i < a + 1, upperCentralSeries G i ∈ upperCentralSeries G '' Set.Iic a

case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (i j : ℕ), i < a + 1 → j < a + 1 → upperCentralSeries G i = upperCentralSeries G j → i = j
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ ⊤.lowerCentralSeries n ≤ pi Set.univ fun i ↦ ⊤.lowerCentralSeries n

Tactic:
rw [← pi_top (I := Set.univ)]
  exact lowerCentralSeries_pi_le _ _

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
g₁ g₂ : G
a : X
ha₁ : a ∈ g₁ • B₁ ∩ g₁ • B₂
ha₂ : a ∈ g₂ • B₁ ∩ g₂ • B₂
⊢ g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂

Tactic:
h₁ ⟨a, ha₁.1, ha₂.1⟩,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
g₁ g₂ : G
a : X
ha₁ : a ∈ g₁ • B₁ ∩ g₁ • B₂
ha₂ : a ∈ g₂ • B₁ ∩ g₂ • B₂
⊢ g₂ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s

Tactic:
rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a✝ : α
⊢ a✝ ∈ (k • g).support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support

Tactic:
mem_conj_support,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a✝ : α
⊢ (ConjAct.ofConjAct k⁻¹) a✝ ∈ g.support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
g : G
hg : a ∈ g • B'
⊢ g ∈ stabilizer G B'

Tactic:
mem_stabilizer_set_iff_subset_smul_set hfB'

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y

Tactic:
rw [eq_iff_true_of_subsingleton]

Goal state after:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ Cardinal.toENat (Cardinal.mk ↥(ofStabilizer G a)) + 1 = Cardinal.toENat (Cardinal.mk α)

Tactic:
← Cardinal.mk_sum_compl {a},

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ Cardinal.toENat (Cardinal.mk ↥(ofStabilizer G a)) + 1 = Cardinal.toENat (Cardinal.mk ↑{a} + Cardinal.mk ↑{a}ᶜ)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card • 2 ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
smul_eq_mul

Goal state after:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Subsingleton
⊢ IsTrivialBlock B

Tactic:
left
    exact h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ k ∈ Perm.ofSubtype.range.subgroupOf (alternatingGroup α) ↔ (↑k).support ⊆ s

Tactic:
mem_subgroupOf,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ ↑k ∈ Perm.ofSubtype.range ↔ (↑k).support ⊆ s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ swap a b ∈ G

Tactic:
rw [← (isConj_iff.mp <| isConj_swap hxy hab).choose_spec]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ ⋯.choose * swap x y * ⋯.choose⁻¹ ∈ G
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
ha : (Classical.choice Hs) i = a
⊢ g • (append x) (castAdd m i) = g • x' (castAdd m i)

Tactic:
← hx

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
ha : (Classical.choice Hs) i = a
⊢ g • x' (castAdd m i) = g • x' (castAdd m i)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mp
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := ⋯
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := ⋯
x : α
⊢ x ∈ s' → x ∈ insert a (Subtype.val '' t)

Tactic:
intro hxs
          by_cases hxa : x = a
          · simp [hxa]
          · exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩

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

Goal state before:
pp: case right.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : ⟨a, ha⟩ ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ False

Tactic:
apply ha'
      simpa only [Set.mem_preimage]

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 α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := ⋯
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := ⋯
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + ↑1 = s.encard

Tactic:
rw [show s = g⁻¹ • s' by simp [hs'],
        ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + ↑1 = (insert a (Subtype.val '' t)).encard