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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : M
⊢ Function.Surjective ⇑(eval IM I M R x)

Tactic:
intro r
  obtain ⟨y, rfl⟩ := smoothSheaf.eval_surjective IM I R x r
  use (smoothSheafCommRing.forgetStalk IM I M R x).inv y
  apply smoothSheafCommRing.forgetStalk_inv_comp_eval_apply

Goal state after:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
⊢ Prod.fst ∘ ⇑h.equiv '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target

Tactic:
by
  rw [← h.writtenInCharts.image_eq, Set.image_comp, Set.image_comp,
    PartialEquiv.symm_image_target_eq_source, OpenPartialHomeomorph.extend_source,
    ← PartialEquiv.image_source_eq_target]
  have : f '' h.domChart.source ⊆ h.codChart.source := by
    simp [h.source_subset_preimage_source]
  grw [this, OpenPartialHomeomorph.extend_source]

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p : Polygon P 3
h : HasNondegenerateVertices R p
⊢ AffineIndependent R p.vertices

Tactic:
by
    have : p.vertices = ![p.vertices 0, p.vertices 1, p.vertices 2] := List.ofFn_inj.mp rfl
    rw [this]
    apply h

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Fintype.card G

Tactic:
← sum_conjClasses_card_eq_card,

Goal state after:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier =
    ∑ x, x.carrier.toFinset.card
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ hi ∈ map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆ → hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆

Tactic:
rw [map_commutator]

Goal state after:
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ hi ∈ ⁅map (MonoidHom.mulSingle Gs i) (H i), map (MonoidHom.mulSingle Gs i) (K i)⁆ →
    hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆
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
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)

Tactic:
cases nonempty_fintype ι
  set F := EuclideanSpace ℝ (Fin <| finrank ℝ (ι → E × ℝ))
  let : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.2 inferInstance
  let : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.1 inferInstance
  set eEF : (ι → E × ℝ) ≃L[ℝ] F :=
    ContinuousLinearEquiv.ofFinrankEq finrank_euclideanSpace_fin.symm
  refine ⟨_, eEF ∘ f.embeddingPiTangent,
    eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
    eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩
  rw [mfderiv_comp _ eEF.differentiableAt.mdifferentiableAt
      (f.embeddingPiTangent.contMDiff.mdifferentiableAt (by simp)),
    eEF.mfderiv_eq]
  exact eEF.injective.comp (f.embeddingPiTangent_injective_mfderiv _ trivial)

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

Goal state before:
pp: case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

pp: case inl
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
· rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]

Goal state after:
case inl
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Tactic:
congr 2

Goal state after:
case e_a
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 } =
    Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })) / ↑(Nat.card ((a : α) → i a)) ^ 2

Tactic:
congr 2

Goal state after:
case e_a
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ Nat.card { p // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x } = Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
⊢ Function.Injective rcons

Tactic:
rintro ⟨m, w, h⟩ ⟨m', w', h'⟩ he
  by_cases hm : m = 1 <;> by_cases hm' : m' = 1
  · simp only [rcons, dif_pos hm, dif_pos hm'] at he
    simp_all
  · exfalso
    simp only [rcons, dif_pos hm, dif_neg hm'] at he
    rw [he] at h
    exact h rfl
  · exfalso
    simp only [rcons, dif_pos hm', dif_neg hm] at he
    rw [← he] at h'
    exact h' rfl
  · have : m = m' ∧ w.toList = w'.toList := by
      simpa [cons, rcons, dif_neg hm, dif_neg hm', eq_self_iff_true, Subtype.mk_eq_mk,
        heq_iff_eq, ← Subtype.ext_iff] using he
    rcases this with ⟨rfl, h⟩
    congr
    exact Word.ext h

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

Goal state before:
pp: case h₁
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.reverse.length
⊢ cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)

Tactic:
length_reverse,

Goal state after:
case h₁
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.length
⊢ cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
ω : List B
hω : cs.IsReduced ω
h'ω : w⁻¹ = cs.wordProd ω
this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.reverse.length
⊢ cs.length w ≤ cs.length w⁻¹

Tactic:
length_reverse,

Goal state after:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
ω : List B
hω : cs.IsReduced ω
h'ω : w⁻¹ = cs.wordProd ω
this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.length
⊢ cs.length w ≤ cs.length w⁻¹
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * (l * (a * (r * r'⁻¹)))

Tactic:
eq_inv_mul_iff_mul_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ y * b = l * (a * (r * r'⁻¹))
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2 ∈ ⊥, ∃ b_1 ∈ H, b = a_2 * a * b_1

Tactic:
rintro (h : a⁻¹ * b ∈ H)
    exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case refine_2
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (CoprodI fun x ↦ FreeGroup Unit) →* FreeGroup ι

pp: case refine_3
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ MonoidHom.comp ?refine_2 (FreeGroup.lift fun i ↦ of (FreeGroup.of ())) = MonoidHom.id (FreeGroup ι)

pp: case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp ?refine_2 = MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)

Tactic:
· exact CoprodI.lift fun i => FreeGroup.lift fun _ => FreeGroup.of i

Goal state after:
case refine_3
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i).comp (FreeGroup.lift fun i ↦ of (FreeGroup.of ())) =
    MonoidHom.id (FreeGroup ι)

case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i) =
    MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : 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
⊢ Function.Injective ⇑(lift fun i ↦ FreeGroup.lift fun x ↦ a i)

Tactic:
change Function.Injective (lift fun i : ι => FreeGroup.lift fun _ => a i)

Goal state after:
ι : 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
⊢ Function.Injective ⇑(lift fun i ↦ FreeGroup.lift fun x ↦ a i)
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
this : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H))
⊢ Nat.card ↥(domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H)

Tactic:
rw [Nat.card_congr (MonoidHom.domRestrictHomKerEquiv Mˣ H).toEquiv,
    card_monoidHom_of_hasEnoughRootsOfUnity]

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (List.map
        (Subtype.val ∘ fun q ↦
          ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩)
        Finset.univ.toList).prod =
    (List.map (Subtype.val ∘ fun i ↦ ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) i.out) Finset.univ.toList).prod

Tactic:
congr 2

Goal state after:
case e_f
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (Subtype.val ∘ fun q ↦
      ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩) =
    Subtype.val ∘ fun i ↦ ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) i.out
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
hN : N.IsFinitelyNormallyGenerated
f : G →* H
hf : Surjective ⇑f
hf' : f.ker.IsFinitelyNormallyGenerated
⊢ (comap f N).IsFinitelyNormallyGenerated

Tactic:
obtain ⟨S, hS_fin, hS⟩ := hN
  obtain ⟨T, hT_fin, hT⟩ := hf'
  have : ∃ S', S'.Finite ∧ f '' S' = S :=
    ⟨surjInv hf '' S, hS_fin.image _, by rw [← image_comp, comp_surjInv, image_id]⟩
  clear hS_fin
  obtain ⟨S, hS_fin, rfl⟩ := this
  refine ⟨S ∪ T, hS_fin.union hT_fin, ?_⟩
  rw [← hS, ← map_normalClosure S f hf, comap_map_eq, ← hT, normalClosure_union]

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      ((center ↥(closureCommutatorRepresentatives G)).index *
          Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) +
        1)
h : Nat.card ↥(_root_.commutator G) = 0
⊢ False

Tactic:
card_commutator_closureCommutatorRepresentatives,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card ↥(_root_.commutator G) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      ((center ↥(closureCommutatorRepresentatives G)).index *
          Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) +
        1)
h : Nat.card ↥(_root_.commutator G) = 0
⊢ False
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ (φ x)⁻¹ * φ y = x⁻¹ * y

Tactic:
eq_inv_mul_iff_mul_eq,

Goal state after:
F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ x * ((φ x)⁻¹ * φ y) = y
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ¬(Nat.card G).minFac ∣ (↑P).index

Tactic:
exact P.not_dvd_index

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ IsCyclicallyReduced (reduceCyclically L)

Tactic:
by
  induction L using List.bidirectionalRec
  case nil => simp
  case singleton => simp
  case cons_append a l b ih =>
    rw [reduceCyclically.cons_append]
    split
    case isTrue => exact ih (h.infix ⟨[a], [b], rfl⟩)
    case isFalse h' =>
      rw [isCyclicallyReduced_cons_append_iff]
      exact ⟨h, by simpa using h'⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
⊢ ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
exact ⟨lowerCentralSeries ⊤, ⟨lowerCentralSeries_isDescendingCentralSeries, h⟩⟩

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
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
⊢ IsBlock G (⋂ i, B i)

Tactic:
by
  simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢
  rintro g₁ g₂ ⟨a, ha₁, ha₂⟩
  simp_rw [fun i ↦ hB i ⟨a, iInter_subset _ i ha₁, iInter_subset _ i ha₂⟩]

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
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ g₁ • Subtype.val '' B ≠ g₂ • Subtype.val '' B → Disjoint (g₁ • Subtype.val '' B) (g₂ • Subtype.val '' B) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq,
    Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective]

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
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : B.Nonempty
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Tactic:
obtain ⟨x, hx⟩ := hB_ne

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
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ B.ncard * (orbit G B).ncard = Nat.card X
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
⊢ k ∈ ConjAct.toConjAct g • ofSubtype.range ↔ k ∈ ofSubtype.range

Tactic:
simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
⊢ ↑((ConjAct.toConjAct g)⁻¹ • k).support ⊆ {x | x ∈ s} ↔ ↑k.support ⊆ {x | x ∈ g • s}
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ orbit (↥N) a = Set.univ

Tactic:
apply Or.resolve_left (isTrivialBlock_of_isBlock (IsBlock.orbit_of_normal a))

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ ¬(orbit (↥N) a).Subsingleton
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ ↑(⟨π * swap a b, ⋯⟩ * ⟨σ, hσ✝⟩ * ⟨π * swap a b, ⋯⟩⁻¹) = ↑⟨τ, hτ⟩

Tactic:
simp only [← hπ, Subgroup.coe_mul]
      have hd : Disjoint (swap a b) σ := by
        rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left,
          Finset.disjoint_singleton_left]
        exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
      simp [mul_assoc, hd.commute.eq]

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

Goal state before:
pp: case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ {(swap 0 4).support.card} + (swap 1 3).cycleType = Multiset.replicate 2 2

pp: case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ (swap 0 4).Disjoint (swap 1 3)

Tactic:
(isCycle_swap h13).cycleType,

Goal state after:
case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ {(swap 0 4).support.card} + {(swap 1 3).support.card} = Multiset.replicate 2 2

case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ (swap 0 4).Disjoint (swap 1 3)
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
h : s = ∅
⊢ n < 1

Tactic:
rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs

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 : 0 = n
h : s = ∅
⊢ n < 1
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr.right
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
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
have : ∃ b : α, b ∈ s := by
        rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
        intro h
        apply not_lt.mpr hn
        rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
        simp only [← hs, zero_lt_one]

Goal state after:
case mpr.right
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
this : ∃ b, b ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
by
      refine ⟨this, fun hs_prim ↦ ?_⟩
      rw [hsa] at hs_prim
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),
        is_one_preprimitive_iff]
      exact IsPreprimitive.of_surjective
          ofFixingSubgroup_of_singleton_bijective.surjective

Goal state after: