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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
⊢ ∃ C > 0, ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C

Tactic:
by
  rcases eventually_norm_mfderivWithin_symm_extChartAt_lt I x with ⟨C, C_pos, hC⟩
  lift C to ℝ≥0 using C_pos.le
  simp only [gt_iff_lt, NNReal.coe_pos] at C_pos
  refine ⟨C, C_pos, ?_⟩
  filter_upwards [hC] with y hy
  simp only [enorm, nnnorm]
  exact_mod_cast hy

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
⊢ ∃ C > 0, ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)

Tactic:
refine ⟨C, C_pos, ?_⟩

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
⊢ ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
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 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
pre_mem : ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
    (fun x₀ ↦ ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
C :
  ContMDiffWithinAt I I.tangent m'
    (fun x_1 ↦
      ⟨x_1,
        mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) x_1⟩)
    s x
⊢ m' + 1 ≠ ∞

Tactic:
simp [h'm']

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

Goal state before:
pp: P : Type u_3
n : ℕ
inst✝ : NeZero n
poly : Polygon P n
h : poly.HasNondegenerateEdges
⊢ 2 ≤ n

Tactic:
by
  by_contra! hlt
  interval_cases n
  · simp_all only [neZero_zero_iff_false]
  · exact h 0 (by simp)

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ x ∈ Finset.univ \ (noncenter G).toFinset, 1 = Fintype.card ↑x.carrier

Tactic:
rintro ⟨g⟩ hg

Goal state after:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ Finset.univ \ (noncenter G).toFinset
⊢ 1 = Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g))
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ ¬4 * (n % 4 * n) * (n / 4 + 1) = 0

Tactic:
· positivity [hn.pos.ne']

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
w : Word M
i : ι
⊢ ¬w.fstIdx ≠ some i ↔ ¬∀ l ∈ w.toList.head?, i ≠ l.fst

Tactic:
simp [fstIdx]

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

Goal state before:
pp: case nil
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.wordProd [].reverse = (cs.wordProd [])⁻¹

Tactic:
| nil =>

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case nil
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
h1 : ∀ l ∈ [], l.snd ≠ 1
h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) []
⊢ motive { toList := [], ne_one := h1, chain_ne := h2 }

Tactic:
| nil =>

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) ≠ cs.length w

Tactic:
← length_inv

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w)⁻¹ ≠ cs.length w
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.rightInvSeq ([].concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq [])).concat (cs.simple i)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.leftInvSeq [] = (cs.rightInvSeq [].reverse).reverse

Tactic:
| nil =>

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

Goal state before:
pp: case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ (cs.rightInvSeq []).length = [].length

Tactic:
| nil =>

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

Goal state before:
pp: case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
⊢ (cs.rightInvSeq []).getD j 1 =
    (cs.wordProd (drop (j + 1) []))⁻¹ * (Option.map cs.simple [][j]?).getD 1 * cs.wordProd (drop (j + 1) [])

Tactic:
| nil =>

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹) < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w

Tactic:
← length_inv

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
⊢ (cs.leftInvSeq []).getD j 1 =
    cs.wordProd (take j []) * (Option.map cs.simple [][j]?).getD 1 * (cs.wordProd (take j []))⁻¹

Tactic:
| nil =>

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

Goal state before:
pp: case succ.nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) []) = drop (j + 1) (cs.rightInvSeq [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : t ∈ cs.rightInvSeq []
⊢ cs.IsReflection t

Tactic:
| nil =>

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case nil
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
hnot1 : ∀ l ∈ [], l.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) []
h : { toList := [], ne_one := hnot1, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := [], ne_one := hnot1, chain_ne := hchain }.toList

Tactic:
| nil =>

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

Goal state before:
pp: case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ (cs.rightInvSeq []).prod = (cs.wordProd [])⁻¹

Tactic:
| nil =>

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ mk m s = mk m' s' ↔ ∃ u, ↑u • ↑s' • m = ↑u • ↑s • m'

Tactic:
unfold mk
  rw [LocalizedModule.mk_eq, ↑ⁿ.exists_congr_left]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
I : Finset (Quotient ↑H ↑K)
hI : ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ
this : ↑I = Set.univ
⊢ Finite (Quotient ↑H ↑K)

Tactic:
by
      simp_rw [← Set.finite_univ_iff, ← this, I.finite_toSet]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ (↑⟨c.den, ⋯⟩ * ↑s * b.num) • m < (↑⟨b.den, ⋯⟩ * ↑s * c.num) • m

Tactic:
PNat.mk_coe

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ (c.den * ↑s * b.num) • m < (b.den * ↑s * c.num) • m
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g •
      (g ^ ((H.quotientEquivSigmaZMod g) (g⁻¹ • g ^ k.cast • Quotient.out q)).snd.cast *
        Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) (g⁻¹ • g ^ k.cast • Quotient.out q)).fst)) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
←
    mul_smul,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g •
      (g ^ ((H.quotientEquivSigmaZMod g) ((g⁻¹ * g ^ k.cast) • Quotient.out q)).snd.cast *
        Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) ((g⁻¹ * g ^ k.cast) • Quotient.out q)).fst)) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬H.index = 0
⊢ g ^ H.index ∈ H

Tactic:
let := fintypeOfIndexNeZero hH

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ H.index ∈ H
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
⊢ g * n * g⁻¹ ∈ H.focalSubgroup

Tactic:
induction hn using closure_induction with
  | mem z hz =>
    obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
  | one => simp
  | mul _ _ _ _ IHa IHb => simpa using mul_mem IHa IHb
  | inv _ _ IH => simpa [mul_assoc] using inv_mem IH

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
rw [isCyclicallyReduced_iff, List.getLast?_concat]

Goal state after:
α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧ ∀ a_1 ∈ some a, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₂ ++ (replicate n L₂).flatten)

Tactic:
rw [← flatten_cons, ← replicate_succ]

Goal state after:
case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (replicate (n + 1) L₂).flatten
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ x✝ * y * x✝⁻¹ = y ↔ y * x✝ = x✝ * y

Tactic:
mul_inv_eq_iff_eq_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ x✝ * y = y * x✝ ↔ y * x✝ = x✝ * y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ ∀ ⦃b : Subgroup G⦄, S ≤ b → (fun S ↦ S.lowerCentralSeries 0) S ≤ (fun S ↦ S.lowerCentralSeries 0) b

Tactic:
T

Goal state after:
case zero
G : Type u_1
inst✝ : Group G
S T : Subgroup G
⊢ S ≤ T → (fun S ↦ S.lowerCentralSeries 0) S ≤ (fun S ↦ S.lowerCentralSeries 0) T
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
d : ℕ
hd : Monotone fun S ↦ S.lowerCentralSeries d
S : Subgroup G
⊢ ∀ ⦃b : Subgroup G⦄, S ≤ b → (fun S ↦ S.lowerCentralSeries (d + 1)) S ≤ (fun S ↦ S.lowerCentralSeries (d + 1)) b

Tactic:
T

Goal state after:
case succ
G : Type u_1
inst✝ : Group G
d : ℕ
hd : Monotone fun S ↦ S.lowerCentralSeries d
S T : Subgroup G
⊢ S ≤ T → (fun S ↦ S.lowerCentralSeries (d + 1)) S ≤ (fun S ↦ S.lowerCentralSeries (d + 1)) T
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.nil
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
⊢ F'.map (homOfPath T Path.nil) = 1

Tactic:
| nil =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
⊢ nilpotencyClass G' ≤ nilpotencyClass G

Tactic:
by
  have := nilpotent_of_surjective _ hf
  rw [nilpotencyClass_def, nilpotencyClass_def]
  classical apply Nat.find_mono
  intro n hn
  rw [eq_top_iff]
  calc
    ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
    _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
    _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
    _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1

Tactic:
by_cases hH : IsNilpotent G

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1

case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨g, hx⟩ := hG x
    obtain ⟨h, hy⟩ := hG y
    exact ⟨h * g⁻¹, by rw [← hx, smul_smul, inv_mul_cancel_right, hy]⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (conjMap hh).comp (conjMap hg) = conjMap hk

Tactic:
ext x
  simpa using conjMap_comp_apply H x

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

Goal state before:
pp: c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ orderOf g' ∣ 2

Tactic:
← lcm_cycleType,

Goal state after:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ g'.cycleType.lcm ∣ 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
φ : Perm α ≃* Perm α
⊢ comap φ.toMonoidHom (alternatingGroup α) = alternatingGroup α

Tactic:
nontriviality α
    apply eq_alternatingGroup_of_index_eq_two
    rw [index_comap_of_surjective _ (Equiv.surjective _), alternatingGroup.index_eq_two]

Goal state after:
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 • ↑((Classical.choice Hs) i) = ↑((Classical.choice Hs) i)

Tactic:
← ofFixingSubgroup.append_left x i

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 • (append x) (castAdd m i) = ↑((Classical.choice Hs) i)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case pos
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'
x : α
hxs : x ∈ s'
hxa : x = a
⊢ x ∈ insert a (Subtype.val '' t)

pp: case neg
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'
x : α
hxs : x ∈ s'
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)

Tactic:
· simp [hxa]

Goal state after:
case neg
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'
x : α
hxs : x ∈ s'
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
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.Finite

Tactic:
exact Set.toFinite s

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
a : α
⊢ k a = ↑g a

Tactic:
obtain ⟨i, rfl⟩ := (hx x) a

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
⊢ k (x.toFun i) = ↑g (x.toFun i)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
y : α
hx : f y ∈ ofFixingSubgroup N t
this : y ∈ ofFixingSubgroup M s
⊢ ∃ a, g a = ⟨f y, hx⟩

Tactic:
by
          exact ⟨⟨y, this⟩, rfl⟩

Goal state after: